{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs               #-}


{-@ LIQUID "--cores=10"            @-}
{-@ LIQUID "--higherorder"         @-}
{-@ LIQUID "--totality"            @-}
{-@ LIQUID "--exactdc"             @-}

module Main where

import Prelude hiding ( mempty, mappend, id, mconcat, map
                      , take, drop  
                      , error, undefined
                      )


import System.Environment   
import Data.String hiding (fromString)
import GHC.TypeLits
import Data.Maybe 

import String
import Language.Haskell.Liquid.ProofCombinators 

import Data.Proxy 

{-@ symbolVal :: forall n proxy. KnownSymbol n => x:proxy n 
  -> {v:String | v == n && v == symbolVal x } @-}
{-@ measure symbolVal :: p n -> String @-}

-------------------------------------------------------------------------------
------------ | String Matching Main Theorem  ----------------------------------
-------------------------------------------------------------------------------

{-@ distributionOfStringMatching :: MI target -> is:SMTString  -> n:Int -> m:Int
   -> {toMI is == pmconcat m (map toMI (chunkString n is))} @-}

distributionOfStringMatching :: forall (target :: Symbol). (KnownSymbol target) => MI target -> SMTString -> Int -> Int -> Proof
distributionOfStringMatching _ is n m  
  =   (pmconcat m (map toMI (chunkString n is)) :: MI target)
  ==. mconcat (map toMI (chunkString n is))
       ? pmconcatEquivalence m (map toMI (chunkString n is) :: List (MI target))
  ==. toMI is 
       ? distributionOfMI (mempty :: MI target) is n 
  *** QED 


-------------------------------------------------------------------------------
------------ | Interface ------------------------------------------------------
-------------------------------------------------------------------------------

main :: IO ()
main = 
  do args      <- getArgs
     case args of 
       (i:fname:target:_) -> do input <- fromString <$> readFile fname 
                                runMatching (read i :: Int) input target
       _                -> putStrLn $ "Wrong input: You need to provide the chunksize," ++
                                      "the input filename and the target string. For example:\n\n\n" ++ 
                                      "./StringIndexing 10 input.txt abcab\n\n"
     

runMatching :: Int -> SMTString -> String -> IO ()
runMatching chunksize input tg =
  case someSymbolVal tg of 
    SomeSymbol (_ :: Proxy target) -> do            
      let mi1    = toMI input :: MI target 
      let is1    = indicesMI mi1 
      putStrLn   $ "Serial   Indices: " ++ show is1
      let mi2    = toMIPar chunksize input :: MI target 
      let is2    = indicesMI mi2 
      putStrLn   $ "Parallel Indices: " ++ show is2
      putStrLn   $ "Are equal? " ++ show (is1 == is2)

test = indicesMI (toMI (fromString $ clone 100 "ababcabcab")  :: MI "abcab" )
  where
    clone i xs = concat (replicate i xs) 



{-@ reflect toMI @-}
toMI :: forall (target :: Symbol). (KnownSymbol target) => SMTString -> MI target 
toMI input  
  | stringLen input == 0 
  = mempty
  | otherwise          
  = MI input (makeIndices input (fromString (symbolVal (Proxy :: Proxy target))) 0 (stringLen input - 1))

toMIPar :: forall (target :: Symbol). (KnownSymbol target) => Int -> SMTString -> MI target  
toMIPar chunksize input 
  = pmconcat chunksize (map toMI (chunkString chunksize input))

-------------------------------------------------------------------------------
----------  Indexing Structure Definition -------------------------------------
-------------------------------------------------------------------------------

data MI (target :: Symbol) where 
  MI :: SMTString       -- | input string
     -> (List Int)      -- | valid indices of target in input
     -> MI target
  deriving (Show)

{-@ data MI target 
  = MI { input   :: SMTString
       , indices :: List (GoodIndex input target)
       } @-}

{-@ type GoodIndex Input Target 
  = {i:Int | IsGoodIndex Input Target i }
  @-}

{-@ type GoodIndexTwo Input X Target 
  = {i:Int | (IsGoodIndex Input Target i)  && (IsGoodIndex (concatString Input X) Target i) }
  @-}


{-@ predicate IsGoodIndex Input Target I
  =  (subString Input I (stringLen Target)  == Target)
  && (I + stringLen Target <= stringLen Input)
  && (0 <= I)
  @-}

{-@ measure indicesMI @-}
indicesMI (MI _ is) = is 

{-@ measure inputMI @-}
inputMI (MI i _) = i 

-------------------------------------------------------------------------------
----------  Monoid Operators on MI --------------------------------------------
-------------------------------------------------------------------------------

{-@ reflect mempty @-}
mempty :: forall (target :: Symbol). (KnownSymbol target) =>  MI target
mempty = MI stringEmp N

{-@ reflect mconcat @-}
mconcat :: forall (target :: Symbol). (KnownSymbol target) => List (MI target) -> MI target 
mconcat N        = mempty
mconcat (C x xs) = mappend x (mconcat xs)

{-@ reflect pmconcat @-}
pmconcat :: forall (target :: Symbol). (KnownSymbol target) => Int -> List (MI target) -> MI target 
{-@ pmconcat :: forall (target :: Symbol). (KnownSymbol target) => 
  Int -> is:List (MI target) -> MI target /[llen is] @-}

pmconcat i xs
  | i <= 1 
  = mconcat xs 
pmconcat i N   
  = mempty
pmconcat i (C x N) 
  = x
pmconcat i xs 
  = pmconcat i (map mconcat (chunk i xs))



{-@ reflect mappend @-}
mappend :: forall (target :: Symbol).  (KnownSymbol target) => MI target -> MI target -> MI target
mappend (MI i1 is1) (MI i2 is2)
  = MI (concatString i1 i2)
       ((castGoodIndexRightList (fromString (symbolVal (Proxy :: Proxy target))) i1 i2 is1
          `append`
        makeNewIndices i1 i2 (fromString (symbolVal (Proxy :: Proxy target)))
       ) `append`
       (map (shiftStringRight (fromString (symbolVal (Proxy :: Proxy target))) i1 i2) is2)) 

-- | Helpers 
{-@ reflect shiftStringRight @-}
shiftStringRight :: SMTString -> SMTString -> SMTString -> Int -> Int 
{-@ shiftStringRight :: target:SMTString -> left:SMTString -> right:SMTString -> i:GoodIndex right target 
  -> {v:(GoodIndex {concatString left right} target) | v == i + stringLen left } @-}
shiftStringRight target left right i 
  = cast (subStringConcatFront right left (stringLen target) i) (shift (stringLen left) i)

{-@ 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 shift @-}
shift :: Int -> Int -> Int 
shift x y = x + y 

-- | Casting good indices: the below operators are liquid casts and behave like id at runtime

-- NV: The recursion is required as there is no other way to (access &) cast _each_ element of the input list
{-@ reflect castGoodIndexRightList @-}
castGoodIndexRightList :: SMTString -> SMTString -> SMTString -> List Int -> List Int    
{-@ castGoodIndexRightList :: target:SMTString -> input:SMTString -> x:SMTString -> is:List (GoodIndex input target) 
    -> {v:List (GoodIndexTwo input x target) | v == is} @-}
castGoodIndexRightList target input x N 
  = N 
castGoodIndexRightList target input x (C i is) 
  = C (castGoodIndexRight target input x i) (castGoodIndexRightList target input x is)  


{-@ reflect castGoodIndexRight @-}
castGoodIndexRight :: SMTString -> SMTString -> SMTString -> Int -> Int  
{-@ castGoodIndexRight :: target:SMTString -> input:SMTString -> x:SMTString -> i:GoodIndex input target 
   -> {v:(GoodIndexTwo input x target)| v == i} @-}
castGoodIndexRight target input x i  = cast (subStringConcatBack input x (stringLen target) i) i


-------------------------------------------------------------------------------
----------  Indices' Generation -----------------------------------------------
-------------------------------------------------------------------------------

{-@ reflect makeIndices @-}
makeIndices :: SMTString -> SMTString -> Int -> Int -> List Int 
{-@ makeIndices :: input:SMTString -> target:SMTString -> lo:Nat -> 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    


-------------------------------------------------------------------------------
----------  List Structure ----------------------------------------------------
-------------------------------------------------------------------------------
   
data List a = N | C a (List a) deriving (Show, Eq)
{-@ data List [llen] a 
  = N | C {lhead :: a , ltail :: List a} @-}


{-@ measure llen @-}
{-@ llen :: List a -> Nat @-} 
llen :: List a -> Int 
llen N        = 0 
llen (C _ xs) = 1 + llen xs 

{-@ reflect map @-}
{-@ map :: (a -> b) -> is:List a -> {os:List b | llen is == llen os} @-}
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        ys = ys 
append (C x xs) ys = x `C` (append xs ys)


{-@ reflect chunk @-}
{-@ chunk :: i:Int -> xs:List a -> {v:List (List a) | if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs) } / [llen xs] @-}
chunk :: Int -> List a -> List (List a)
chunk i xs 
  | i <= 1
  = C xs N 
  | llen xs <= i 
  = C xs N 
  | otherwise
  = C (take i xs) (chunk i (drop i xs))

{-@ reflect drop @-}
{-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-} 
drop :: Int -> List a -> List a 
drop i N = N 
drop i (C x xs)
  | i == 0 
  = C x xs  
  | otherwise 
  = drop (i-1) xs 

{-@ reflect take @-}
{-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-} 
take :: Int -> List a -> List a 
take i N = N 
take i (C x xs)
  | i == 0 
  = N  
  | otherwise 
  = C x (take (i-1) xs)


-------------------------------------------------------------------------------
----------  String Chunking ---------------------------------------------------
-------------------------------------------------------------------------------

{-@ reflect chunkString @-}
{-@ chunkString :: Int -> xs:SMTString -> List (SMTString) / [stringLen xs] @-}
chunkString :: Int -> SMTString -> List (SMTString)
chunkString i xs 
  | i <= 1
  = C xs N 
  | stringLen xs <= i 
  = C xs N 
  | otherwise
  = C (takeString i xs) (chunkString i (dropString i xs))


-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
------------ Liquid Proofs Start HERE -----------------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------


-------------------------------------------------------------------------------
----------  Proof that toMI distributes ---------------------------------------
-------------------------------------------------------------------------------

{-@ distributionOfMI :: MI target -> is:SMTString -> n:Int -> {toMI is == mconcat (map toMI (chunkString n is))} @-}

distributionOfMI :: forall (target :: Symbol). (KnownSymbol target) => MI target -> SMTString -> Int -> Proof
distributionOfMI _ is n = distributeInput (toMI :: SMTString -> MI target) (distributestoMI (mempty :: MI target)) is n 


{-@ distributeInput
     :: f:(SMTString -> MI target)
     -> thm:(x1:SMTString -> x2:SMTString -> {f (concatString x1 x2) == mappend (f x1) (f x2)} )
     -> is:SMTString
     -> n:Int 
     -> {f is == mconcat (map f (chunkString n is))}
     / [stringLen is] 
  @-}

distributeInput :: forall (target :: Symbol). (KnownSymbol target) 
  => (SMTString -> MI target)
  -> (SMTString -> SMTString -> Proof)
  -> SMTString -> Int -> Proof
distributeInput f thm is n  
  | stringLen is <= n || n <= 1
  =   mconcat (map f (chunkString n is))
  ==. mconcat (map f (C is N))
  ==. mconcat (f is `C` map f N)
  ==. mconcat (f is `C` N)
  ==. mappend (f is) (mconcat N)
  ==. mappend (f is) (mempty :: MI target)
  ==. f is ? mempty_left (f is)
  *** QED 
  | otherwise
  =   mconcat (map f (chunkString n is))
  ==. mconcat (map f (C (takeString n is) (chunkString n (dropString n is)))) 
  ==. mconcat (f (takeString n is) `C` map f (chunkString n (dropString n is)))
  ==. mappend (f (takeString n is)) (mconcat (map f (chunkString n (dropString n is))))
  ==. mappend (f (takeString n is)) (f (dropString n is))
       ? distributeInput f thm (dropString n is) n  
  ==. f (concatString (takeString n is) (dropString n is))
       ? thm (takeString n is) (dropString n is)
  ==. f is 
       ? concatTakeDrop n is 
  *** QED 



distributestoMI :: forall (target :: Symbol). (KnownSymbol target) => MI target -> SMTString -> SMTString -> Proof 
{-@ distributestoMI :: MI target -> x1:SMTString -> x2:SMTString -> {toMI (concatString x1 x2) == mappend (toMI x1) (toMI x2)} @-} 
distributestoMI _ x1 x2
  | stringLen x1 == 0, stringLen x2 == 0 
  =   mappend (toMI x1) (toMI x2)
  ==. mappend (mempty :: MI target) (mempty :: MI target)
       ? mempty_left (mempty :: MI target) 
  ==. (mempty :: MI target)
  ==. toMI (concatString x1 x2)
  *** QED 

distributestoMI _ x1 x2
  | stringLen x1 == 0 
  =   mappend (toMI x1) (toMI x2)
  ==. mappend (mempty :: MI target) (toMI x2 :: MI target)
  ==. toMI x2 
      ? mempty_right (toMI x2 :: MI target)
  ==. toMI (concatString x1 x2)
      ? concatEmpLeft x1 x2 
  *** QED 

distributestoMI _ x1 x2
  | stringLen x2 == 0 
  =   mappend (toMI x1) (toMI x2)
  ==. mappend (toMI x1) (mempty :: MI target)
  ==. (toMI x1 :: MI target)
      ? mempty_left (toMI x1 :: MI target)
  ==. toMI (concatString x1 x2)
      ? concatEmpRight x1 x2 
  *** QED 

distributestoMI _ x1 x2 
  | stringLen (fromString (symbolVal (Proxy :: Proxy target))) < 2 
  =   let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend (toMI x1 :: MI target) (toMI x2 :: MI target)  
  ==. mappend (MI x1 (makeIndices x1 tg 0 (stringLen x1 - 1)))
              (MI x2 (makeIndices x2 tg 0 (stringLen x2 - 1)))
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeNewIndices x1 x2 tg
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           N
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         (castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
           `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
      ? appendNil (castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1)))
  ==. MI (concatString x1 x2)
         (castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
           `append`
          (makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen x1 + stringLen x2 -1))) 
      ? shiftIndexesRight' 0 (stringLen x2 - 1) x1 x2 tg 
  ==. MI (concatString x1 x2)
         ( (makeIndices (concatString x1 x2) tg 0 (stringLen x1 - 1))
           `append`
          (makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen x1 + stringLen x2 -1))) 
      ? (concatmakeNewIndices 0 (stringLen x1 -1) tg x1 x2) 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 - 1)
           `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen x1 + stringLen x2 -1)) 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 - 1)
           `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen (concatString x1 x2) -1)) 
  ==. MI (concatString x1 x2) 
         (makeIndices (concatString x1 x2) tg 0 (stringLen (concatString x1 x2) - 1))
      ? mergeIndices (concatString x1 x2) tg 0 (stringLen x1 -1) (stringLen (concatString x1 x2) - 1) 
  ==. toMI (concatString x1 x2)
  *** QED 

distributestoMI _ x1 x2
  | 0 <= stringLen x1 - stringLen (fromString (symbolVal (Proxy :: Proxy target))) 
  =   let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend (toMI x1 :: MI target) (toMI x2:: MI target)  
  ==. mappend (MI x1 (makeIndices x1 tg 0 (stringLen x1 - 1)))
              (MI x2 (makeIndices x2 tg 0 (stringLen x2 - 1)))
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeNewIndices x1 x2 tg
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeIndices (concatString x1 x2) tg (maxInt (stringLen x1 - stringLen tg +1) 0) (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeIndices (concatString x1 x2) tg (stringLen x1 - stringLen tg +1) (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((makeIndices (concatString x1 x2) tg 0 (stringLen x1 - stringLen tg)
          `append`
           makeIndices (concatString x1 x2) tg (stringLen x1 - stringLen tg +1) (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
         ? catIndices x1 x2 tg 0 (stringLen x1 -1 ) -- HERE HERE requires stringLen tg <= stringLen x1
  ==. MI (concatString x1 x2)
         ((makeIndices (concatString x1 x2) tg 0 (stringLen x1 - stringLen tg)
          `append`
           makeIndices (concatString x1 x2) tg (stringLen x1 - stringLen tg +1) (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
         `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
          ? mergeIndices (concatString x1 x2) tg 0 (stringLen x1 -stringLen tg) (stringLen x1-1)
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
         `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen x1 + stringLen x2 - 1))
          ? shiftIndexesRight' 0 (stringLen x2 -1) x1 x2 tg 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
         `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen (concatString x1 x2) - 1))
  ==. MI (concatString x1 x2) 
         (makeIndices (concatString x1 x2) tg 0 (stringLen (concatString x1 x2) - 1))
          ? mergeIndices (concatString x1 x2) tg 0 (stringLen x1- 1) (stringLen (concatString x1 x2) - 1)
  ==. toMI (concatString x1 x2)
  *** QED 
distributestoMI _ x1 x2
  | stringLen x1 - stringLen (fromString (symbolVal (Proxy :: Proxy target))) < 0 
  =   let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend (toMI x1 :: MI target) (toMI x2:: MI target)  
  ==. mappend (MI x1 (makeIndices x1 tg 0 (stringLen x1 - 1)))
              (MI x2 (makeIndices x2 tg 0 (stringLen x2 - 1)))
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeNewIndices x1 x2 tg
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeIndices (concatString x1 x2) tg (maxInt (stringLen x1 - stringLen tg +1) 0) (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         ((castGoodIndexRightList tg x1 x2 (makeIndices x1 tg 0 (stringLen x1 - 1))
          `append`
           makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
          
  ==. MI (concatString x1 x2)
         ((N
          `append`
           makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
          ) `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
         ? makeNewIndicesNullSmallInput x1 tg 0 (stringLen x1 - 1)  
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
           `append`
          (map (shiftStringRight tg x1 x2) (makeIndices x2 tg 0 (stringLen x2 - 1)))) 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
         `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen x1 + stringLen x2 - 1))
          ? shiftIndexesRight' 0 (stringLen x2 -1) x1 x2 tg 
  ==. MI (concatString x1 x2)
         (makeIndices (concatString x1 x2) tg 0 (stringLen x1 -1)
         `append`
          makeIndices (concatString x1 x2) tg (stringLen x1) (stringLen (concatString x1 x2) - 1))
  ==. MI (concatString x1 x2) 
         (makeIndices (concatString x1 x2) tg 0 (stringLen (concatString x1 x2) - 1))
          ? mergeIndices (concatString x1 x2) tg 0 (stringLen x1- 1) (stringLen (concatString x1 x2) - 1)
  ==. toMI (concatString x1 x2)
  *** QED 

-------------------------------------------------------------------------------
----------  Parallelization: pmconcat i is == mconcat is ----------------------
-------------------------------------------------------------------------------

pmconcatEquivalence :: forall (target :: Symbol). (KnownSymbol target) => Int -> List (MI target) -> Proof
{-@ pmconcatEquivalence :: i:Int -> is:List (MI target) -> {pmconcat i is == mconcat is} / [llen is] @-}
pmconcatEquivalence i is 
  | i <= 1
  = pmconcat i is ==. mconcat is *** QED 
pmconcatEquivalence i N 
  =   pmconcat i N 
  ==. (mempty :: MI target) 
  ==. mconcat N 
  *** QED 
pmconcatEquivalence i (C x N) 
  =   pmconcat i (C x N)
  ==. x 
  ==. mappend x mempty 
      ? mempty_left x
  ==. mappend x (mconcat N) 
  ==. mconcat (C x N) 
  *** QED 
pmconcatEquivalence i xs 
  | llen xs <= i 
  =   pmconcat i xs 
  ==. pmconcat i (map mconcat (chunk i xs))
  ==. pmconcat i (map mconcat (C xs N))
  ==. pmconcat i (mconcat xs `C`  map mconcat N)
  ==. pmconcat i (mconcat xs `C`  N)
  ==. mconcat xs
  *** QED 
pmconcatEquivalence i xs
  =   pmconcat i xs 
  ==. pmconcat i (map mconcat (chunk i xs))
  ==. mconcat (map mconcat (chunk i xs))
       ? pmconcatEquivalence i (map mconcat (chunk i xs))
  ==. mconcat xs
       ? mconcatAssoc i xs
  *** QED 

-- | Monoid implications 

mconcatAssocOne :: forall (target :: Symbol). (KnownSymbol target) => Int -> List (MI target) -> Proof 
{-@ mconcatAssocOne :: i:Nat -> xs:{List (MI target) | i <= llen xs} 
     -> {mconcat xs == mappend (mconcat (take i xs)) (mconcat (drop i xs))}
     /[i]
  @-} 
mconcatAssocOne i N 
  =   mappend (mconcat (take i N)) (mconcat (drop i N)) 
  ==. mappend (mconcat N) (mconcat N)
  ==. mappend (mempty :: MI target) (mempty :: MI target)
  ==. (mempty :: MI target) 
      ? mempty_left  (mempty :: MI target)
  ==. mconcat N 
  *** QED 

mconcatAssocOne i (C x xs)
  | i == 0
  =   mappend (mconcat (take i (C x xs))) (mconcat (drop i (C x xs))) 
  ==. mappend (mconcat N) (mconcat (C x xs))
  ==. mappend mempty (mconcat (C x xs))
  ==. mconcat (C x xs)
      ? mempty_right (mconcat (C x xs))
  *** QED 
  | otherwise    
  =   mappend (mconcat (take i (C x xs))) (mconcat (drop i (C x xs))) 
  ==. mappend (mconcat (C x (take (i-1) xs))) (mconcat (drop (i-1) xs))
  ==. mappend (mappend x (mconcat (take (i-1) xs))) (mconcat (drop (i-1) xs))
       ? mappend_assoc x (mconcat (take (i-1) xs)) (mconcat (drop (i-1) xs))
  ==. mappend x (mappend (mconcat (take (i-1) xs)) (mconcat (drop (i-1) xs)))
       ? mconcatAssocOne (i-1) xs
  ==. mappend x (mconcat xs)
  ==. mconcat (C x xs)
  *** QED 

-- Generalization to chunking  

mconcatAssoc :: forall (target :: Symbol). (KnownSymbol target) => Int -> List (MI target) -> Proof 
{-@ mconcatAssoc :: i:Int -> xs:List (MI target) 
  -> { mconcat xs == mconcat (map mconcat (chunk i xs))}
  /  [llen xs] @-}
mconcatAssoc i xs  
  | i <= 1 || llen xs <= i
  =   mconcat (map mconcat (chunk i xs))
  ==. mconcat (map mconcat (C xs N))
  ==. mconcat (mconcat xs `C` map mconcat N)
  ==. mconcat (mconcat xs `C` N)
  ==. mappend (mconcat xs) (mconcat N)
  ==. mappend (mconcat xs) (mempty :: MI target)
  ==. mconcat xs 
       ? mempty_left (mconcat xs)
  *** QED  
   | otherwise
   =   mconcat (map mconcat (chunk i xs))
   ==. mconcat (map mconcat (take i xs `C` chunk i (drop i xs)))
   ==. mconcat (mconcat (take i xs) `C` map mconcat (chunk i (drop i xs)))
   ==. mappend (mconcat (take i xs)) (mconcat (map mconcat (chunk i (drop i xs))))
   ==. mappend (mconcat (take i xs)) (mconcat (drop i xs))
        ? mconcatAssoc i (drop i xs)
   ==. mconcat xs 
        ? mconcatAssocOne i xs 
   *** QED 


-------------------------------------------------------------------------------
----------  Proof that MI is a Monoid -----------------------------------------
-------------------------------------------------------------------------------

mempty_left :: forall (target :: Symbol). (KnownSymbol target) => MI target -> Proof
{-@ mempty_left :: xs:MI target -> {mappend xs mempty == xs } @-}
mempty_left (MI i1 is1) 
  = let tg = fromString (symbolVal (Proxy :: Proxy target)) in 
      mappend (MI i1 is1) (mempty :: MI target)
  ==. mappend (MI i1 is1) (MI stringEmp N) 
  ==. MI (concatString i1 stringEmp)
         ((castGoodIndexRightList tg i1 stringEmp is1
            `append`
           makeNewIndices i1 stringEmp tg 
         ) `append`
         (map (shiftStringRight tg i1 stringEmp) N))
      ? concatStringNeutralLeft i1 
        -- NV ordering is important! 
        -- concatString i1 stringEmp == i1 should come before application of MI
  ==. MI i1
         ((castGoodIndexRightList tg i1 stringEmp is1
            `append`
           makeNewIndices i1 stringEmp tg
         ) `append`
         (map (shiftStringRight tg i1 stringEmp) N))
  ==. MI i1 ((is1 `append` N) `append` (map (shiftStringRight tg i1 stringEmp) N))
      ? makeNewIndicesNullLeft i1 tg 
  ==. MI i1 (is1 `append` map (shiftStringRight tg i1 stringEmp) N)
      ? appendNil is1  
  ==. MI i1 (is1 `append` N)
      ? appendNil is1  
  ==. MI i1 is1 
  *** QED 

mempty_right :: forall (target :: Symbol). (KnownSymbol target) => MI target -> Proof
{-@ mempty_right :: xs:MI target -> {mappend mempty xs == xs } @-}
mempty_right (MI i is)
  =   let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend (mempty :: MI target) (MI i is) 
  ==. mappend (MI stringEmp N) (MI i is) 
  ==. MI (concatString stringEmp i)
       ((castGoodIndexRightList tg stringEmp i N
          `append`
        makeNewIndices stringEmp i tg 
       ) `append`
       (map (shiftStringRight tg stringEmp i) is)) 
       ? concatStringNeutralRight i
  ==. MI i
        ((N`append` makeNewIndices stringEmp i tg
        ) `append`
        (map (shiftStringRight tg stringEmp i) is)) 
  ==. MI i
       (makeNewIndices stringEmp i tg
        `append`
       (map (shiftStringRight tg stringEmp i) is)) 
  ==. MI i (N `append` (map (shiftStringRight tg stringEmp i) is)) 
       ? makeNewIndicesNullRight i tg
  ==. MI i (map (shiftStringRight tg stringEmp i) is)
       ? mapShiftZero tg i is 
  ==. MI i is 
  *** QED 

{-@ mappend_assoc :: x:MI target -> y:MI target -> z:MI target
  -> { mappend x (mappend y z) = mappend (mappend x y) z}
  @-}
mappend_assoc 
     :: forall (target :: Symbol). (KnownSymbol target) 
     => MI target ->  MI target ->  MI target -> Proof
mappend_assoc x@(MI xi xis) y@(MI yi yis) z@(MI zi zis)
  | stringLen (fromString (symbolVal (Proxy :: Proxy target))) <= stringLen yi 
  = let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend x (mappend y z)
  ==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
  ==. mappend (MI xi xis) 
              (MI (concatString yi zi)
                  ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis)))
  ==. MI (concatString xi (concatString yi zi))
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis))))
      ? concatStringAssoc xi yi zi 
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis))))
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ))
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
      ? mapAppend (shiftStringRight tg xi (concatString yi zi))
                  (castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   )
                   (map (shiftStringRight tg yi zi) zis)
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis)
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
      ? mapAppend (shiftStringRight tg xi (concatString yi zi))
                  (castGoodIndexRightList tg yi zi yis)
                  (makeNewIndices yi zi tg)
-- ((x1~x2) ~ (x3~x4)) ~ x5
-- == 
-- (x1~x2) ~ x3 ~ x4 ~ x5 

  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis))
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
      ? appendReorder (castGoodIndexRightList tg xi (concatString yi zi) xis)
                      (makeNewIndices xi (concatString yi zi) tg)
                      (map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis))
                      (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
                      (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))

  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis) 
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis))
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
      ? castConcat tg xi yi zi xis 
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
           `append`
           castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
          ) `append`
          map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis))
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
      ? shiftIndexesLeft xi yi zi tg 
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
           `append`
           castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
          ) `append`
          castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis))
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
         ? castEq3 tg xi yi zi yis 
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
           `append`
           castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
          ) `append`
          castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis))
            `append`
           makeNewIndices (concatString xi yi) zi tg
           )
            `append`
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
         ? shiftIndexesRight xi yi zi tg 
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
           `append`
           castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
          ) `append`
          castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis))
            `append`
           makeNewIndices (concatString xi yi) zi tg
           )
            `append`
           map (shiftStringRight tg (concatString xi yi) zi) zis)
         ? mapLenFusion tg xi yi zi zis 
  ==. MI (concatString (concatString xi yi) zi)
         (((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
              `append`
           castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
           ) `append`
           castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis)
            `append`
          makeNewIndices (concatString xi yi) zi tg
          ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
        ? castAppend tg (concatString xi yi) zi 
                     (castGoodIndexRightList tg xi yi xis)
                     (makeNewIndices xi yi tg)
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis)
            `append`
          makeNewIndices (concatString xi yi) zi tg
         ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
        ? castAppend tg (concatString xi yi) zi 
             (castGoodIndexRightList tg xi yi xis
              `append`
             makeNewIndices xi yi tg
             )
             (map (shiftStringRight tg xi yi) yis)
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           (map (shiftStringRight tg xi yi) yis))
            `append`
          makeNewIndices (concatString xi yi) zi tg
         ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
  ==. mappend (
        MI (concatString xi yi)
           ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           (map (shiftStringRight tg xi yi) 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))) 
  = let tg = (fromString (symbolVal (Proxy :: Proxy target))) in 
      mappend x (mappend y z)
  ==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
  ==. mappend (MI xi xis) 
              (MI (concatString yi zi)
                  ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis)))
  ==. MI (concatString xi (concatString yi zi))
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis))))
      ? concatStringAssoc xi yi zi 
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) ((castGoodIndexRightList tg yi zi yis
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis))))
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) ((castGoodIndexRightList tg yi zi N
                     `append`
                   makeNewIndices yi zi tg
                   ) `append`
                  (map (shiftStringRight tg yi zi) zis))))
        ? emptyIndices y yis
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) (
                   makeNewIndices yi zi tg
                   `append`
                  (map (shiftStringRight tg yi zi) zis))))
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg xi (concatString yi zi) xis
           `append`
           makeNewIndices xi (concatString yi zi) tg
          ) `append`
          (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg) 
             `append` 
           map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis)))
      ? mapAppend (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg) (map (shiftStringRight tg yi zi) zis)
  ==. MI (concatString (concatString xi yi) zi)
         (((castGoodIndexRightList tg xi (concatString yi zi) xis)
           `append`
           ((makeNewIndices xi (concatString yi zi) tg)
           `append`
           (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))))
            `append`
           (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis)))
      ? appendGroupNew (castGoodIndexRightList tg xi (concatString yi zi) xis)
                       (makeNewIndices xi (concatString yi zi) tg)
                       (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
                       (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
  ==. MI (concatString (concatString xi yi) zi)
         ( (castGoodIndexRightList tg xi (concatString yi zi) xis)
           `append`
           ((castGoodIndexRightList tg (concatString xi yi) zi ((makeNewIndices xi yi) tg))
           `append`
           (makeNewIndices (concatString xi yi) zi tg))
            `append`
           (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis)))
      ? shiftNewIndices xi yi zi tg 
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg xi (concatString yi zi) xis)
           `append`
           (castGoodIndexRightList tg (concatString xi yi) zi ((makeNewIndices xi yi) tg)))
           `append`
           (makeNewIndices (concatString xi yi) zi tg))
            `append`
           (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis)))
      ? appendUnGroupNew (castGoodIndexRightList tg xi (concatString yi zi) xis)
                         (castGoodIndexRightList tg (concatString xi yi) zi ((makeNewIndices xi yi) tg))
                         (makeNewIndices (concatString xi yi) zi tg)
                         (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis))
  ==. MI (concatString (concatString xi yi) zi)
         ((((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis))
           `append`
           (castGoodIndexRightList tg (concatString xi yi) zi ((makeNewIndices xi yi) tg)))
           `append`
           (makeNewIndices (concatString xi yi) zi tg))
            `append`
           (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis)))
      ? castConcat tg xi yi zi xis 
  ==. MI (concatString (concatString xi yi) zi)
         ( ((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
            `append`
             castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)
           )
            `append`
          makeNewIndices (concatString xi yi) zi tg
           ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
      ? mapLenFusion tg xi yi zi zis 
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           )
            `append`
          makeNewIndices (concatString xi yi) zi tg
           ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
      ? castAppend tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis) (makeNewIndices xi yi tg)
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           N)
            `append`
          makeNewIndices (concatString xi yi) zi tg
         ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
         ? appendNil (castGoodIndexRightList tg xi yi xis `append` makeNewIndices xi yi tg)
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           (map (shiftStringRight tg xi yi) N))
            `append`
          makeNewIndices (concatString xi yi) zi tg
         ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
  ==. MI (concatString (concatString xi yi) zi)
         ((castGoodIndexRightList tg (concatString xi yi) zi ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           (map (shiftStringRight tg xi yi) yis))
            `append`
          makeNewIndices (concatString xi yi) zi tg
         ) `append`
         (map (shiftStringRight tg (concatString xi yi) zi) zis)) 
         ? emptyIndices y yis 
  ==. mappend (
        MI (concatString xi yi)
           ((castGoodIndexRightList tg xi yi xis
              `append`
            makeNewIndices xi yi tg
           ) `append`
           (map (shiftStringRight tg xi yi) yis))) (MI zi zis) 
  ==. mappend (mappend (MI xi xis) (MI yi yis)) (MI zi zis)
  *** QED 

-------------------------------------------------------------------------------
----------  Lemmata on Casts --------------------------------------------------
-------------------------------------------------------------------------------

{-@ castAppend :: target:SMTString -> input:SMTString -> x:SMTString 
     -> is1:List (GoodIndex input target) 
     -> is2:List (GoodIndex input target) -> 
   {castGoodIndexRightList target input x (append is1 is2) == append (castGoodIndexRightList target input x is1) (castGoodIndexRightList target input x is2)}
    @-}
castAppend :: SMTString -> SMTString -> SMTString -> List Int -> List Int -> Proof 
castAppend target input x is1 is2 
  =   castGoodIndexRightList target input x (append is1 is2)
  ==. append is1 is2 
  ==. append (castGoodIndexRightList target input x is1) (castGoodIndexRightList target input x is2)
  *** QED 

castConcat :: SMTString -> SMTString -> SMTString -> SMTString -> List Int -> Proof
{-@ castConcat :: tg:SMTString -> xi:SMTString -> yi:SMTString -> zi:SMTString 
             ->  xis:List (GoodIndex xi tg) 
        -> {castGoodIndexRightList tg xi (concatString yi zi) xis == castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)} @-}
castConcat tg xi yi zi xis 
  =   castGoodIndexRightList tg xi (concatString yi zi) xis
  ==. xis 
  ==. castGoodIndexRightList tg xi yi xis
  ==. castGoodIndexRightList tg (concatString xi yi) zi (castGoodIndexRightList tg xi yi xis)
  *** QED 


castEq3 :: SMTString -> SMTString -> SMTString -> SMTString -> List Int -> Proof
{-@ castEq3 :: tg:SMTString -> xi:SMTString -> yi:SMTString -> zi:SMTString 
             ->  yis:List (GoodIndex yi tg) 
        -> {castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis) == map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis)} @-}
castEq3 tg xi yi zi yis 
  =   castGoodIndexRightList tg (concatString xi yi) zi (map (shiftStringRight tg xi yi) yis)
  ==. map (shiftStringRight tg xi yi) yis 
  ==. map (shiftStringRight tg xi (concatString yi zi)) (castGoodIndexRightList tg yi zi yis)
        ? mapShiftIndex tg xi yi zi yis 
  *** QED 


-------------------------------------------------------------------------------
----------  Lemmata on Lists --------------------------------------------------
-------------------------------------------------------------------------------

{-@ appendNil :: xs:List a -> { append xs N = xs } @-} 
appendNil :: List a -> Proof 
appendNil N 
  =   append N N
  ==. N
  *** QED 
appendNil (C x xs) 
  =   append (C x xs) N
  ==. C x (append xs N)
  ==. C x xs ? appendNil xs 
  *** 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 

{-@ 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 


mapAppend :: (a -> b) -> List a -> List a -> Proof
{-@ mapAppend 
     :: f:(a -> b) -> xs:List a -> ys:List a 
     -> {map f (append xs ys) == append (map f xs) (map f ys)}
  @-}
mapAppend f N ys 
  =   map f (append N ys)
  ==. map f ys 
  ==. append N (map f ys)
  ==. append (map f N) (map f ys)
  *** QED 
mapAppend 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))
      ? mapAppend f xs ys 
  ==. append (f x `C` map f xs) (map f ys)
  ==. append (map f (x `C` xs)) (map f ys)
  *** QED 


-------------------------------------------------------------------------------
----------  Lemmata on Empty Indices ------------------------------------------
-------------------------------------------------------------------------------

emptyIndices :: forall (target :: Symbol). (KnownSymbol target) => MI target -> List Int  -> Proof
{-@ emptyIndices :: mi:MI target
                 -> is:{List (GoodIndex (inputMI mi) target) | is == indicesMI mi && stringLen (inputMI mi) < stringLen target}
                 -> { is == N } @-}
emptyIndices (MI _ _) N 
  = trivial 
emptyIndices (MI _ _) (C _ _)
  = trivial 

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) 
                   ? concatStringNeutralLeft s
  ==. makeIndices s t
                   0
                   (stringLen s - 1)
  ==. N ? makeNewIndicesNullSmallInput 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) ? concatStringNeutralLeft s 
  ==. N ? makeNewIndicesNullSmallIndex s t (1 + stringLen s - stringLen t) (stringLen s - 1)
  *** QED 

makeNewIndicesNullSmallInput :: SMTString -> SMTString -> Int -> Int -> Proof 
{-@ makeNewIndicesNullSmallInput 
  :: s:SMTString 
  -> t:{SMTString | 1 + stringLen s <= stringLen t } 
  -> lo:Nat 
  -> hi:Int
  -> {makeIndices s t lo hi == N } / [hi - lo] @-} 
makeNewIndicesNullSmallInput 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 ? makeNewIndicesNullSmallInput s1 t (lo+1) hi
  *** QED 


makeNewIndicesNullSmallIndex :: SMTString -> SMTString -> Int -> Int -> Proof 
{-@ makeNewIndicesNullSmallIndex 
  :: s:SMTString 
  -> t:{SMTString | stringLen t < 2 + stringLen s } 
  -> lo:{Nat | 1 + stringLen s - stringLen t <= lo  } 
  -> hi:{Int | lo <= hi}
  -> {makeIndices s t lo hi == N } / [hi - lo] @-} 
makeNewIndicesNullSmallIndex 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 ? makeNewIndicesNullSmallIndex s1 t (lo+1) hi
  *** 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  
  *** QED

-------------------------------------------------------------------------------
----------  Lemmata on Shifting Indices ---------------------------------------
-------------------------------------------------------------------------------

mapLenFusion :: SMTString -> SMTString -> SMTString -> SMTString -> List Int -> Proof
{-@ mapLenFusion :: tg:SMTString -> xi:SMTString -> yi:SMTString -> zi:SMTString 
            -> zis:List (GoodIndex zi tg) 
        -> {map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) zis) == map (shiftStringRight tg (concatString xi yi) zi) zis} 
        / [llen zis ] @-}
mapLenFusion tg xi yi zi N  
  =   map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) N)
  ==. map (shiftStringRight tg xi (concatString yi zi)) N 
  ==. N 
  ==. map (shiftStringRight tg (concatString xi yi) zi) N 
  *** QED  
mapLenFusion tg xi yi zi (C i is)  
  =   map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) (C i is))
  ==. map (shiftStringRight tg xi (concatString yi zi)) (shiftStringRight tg yi zi i `C` map (shiftStringRight tg yi zi) is)
  ==. shiftStringRight tg xi (concatString yi zi) (shiftStringRight tg yi zi i) `C` (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) is))
  ==. shiftStringRight tg (concatString xi yi) zi i `C` (map (shiftStringRight tg xi (concatString yi zi)) (map (shiftStringRight tg yi zi) is))
  ==. shiftStringRight tg (concatString xi yi) zi i `C` (map (shiftStringRight tg (concatString xi yi) zi) is)
       ? mapLenFusion tg xi yi zi is 
  ==. map (shiftStringRight tg (concatString xi yi) zi) (C i is)
  *** QED  

{-@ shiftIndexesRight
  :: xi:SMTString 
  -> yi:SMTString 
  -> zi:SMTString 
  -> tg:{SMTString | stringLen tg <= stringLen yi } 
  -> { map (shiftStringRight tg xi (concatString yi zi)) (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 (shiftStringRight tg xi (concatString yi zi)) N
  ==. map (shiftStringRight tg xi (concatString yi zi)) (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 (shiftStringRight tg xi (concatString yi zi)) (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 (shiftStringRight tg xi (concatString yi zi)) 
               (makeIndices (concatString yi zi) tg 
                             (maxInt (stringLen yi - (stringLen tg -1)) 0)
                             (stringLen yi -1))
  ==. map (shiftStringRight tg xi (concatString yi zi)) 
          (makeNewIndices yi zi tg)
  *** QED

{-@ shiftIndexesRight'
  :: lo:Nat 
  -> hi:Int  
  -> x:SMTString 
  -> input:SMTString 
  -> target:SMTString
  -> { map (shiftStringRight target x input) (makeIndices input target lo hi) == makeIndices (concatString x input) target (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 (shiftStringRight target x input) (makeIndices input target lo hi)
  ==. map (shiftStringRight target x input) N
  ==. N
  ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
  *** QED 
  | lo == hi, isGoodIndex input target lo 
  =   map (shiftStringRight target x input) (makeIndices input target lo hi)
  ==. map (shiftStringRight target x input) (lo `C` N)
  ==. (shiftStringRight target x input lo) `C` (map (shiftStringRight target x input) 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 (shiftStringRight target x input) (makeIndices input target lo hi)
  ==. map (shiftStringRight target x input) 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 (shiftStringRight target x input) (makeIndices input target lo hi)
  ==. map (shiftStringRight target x input) (lo `C` makeIndices input target (lo+1) hi)
  ==. (shiftStringRight target x input lo) `C` (map (shiftStringRight target x input) (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 (shiftStringRight target x input) (makeIndices input target lo hi)
  ==. map (shiftStringRight target x input) (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 


{-@ shiftIndexesLeft
  :: xi:SMTString 
  -> yi:SMTString 
  -> zi:SMTString 
  -> tg:{SMTString | stringLen tg <= stringLen yi } 
  -> {  makeNewIndices xi (concatString yi zi) tg == castGoodIndexRightList tg (concatString xi yi) zi (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 
  ==. castGoodIndexRightList tg (concatString xi yi) zi (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 
  ==. castGoodIndexRightList 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)   
      ? (subStringConcatBack 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 ) &&& (concatLen input input') *** QED))
  ==. isGoodIndex (concatString input input') tg i 
  *** QED 


mapShiftZero :: SMTString -> SMTString -> List Int -> Proof
{-@ mapShiftZero :: target:SMTString -> i:SMTString -> is:List (GoodIndex i target) 
  -> {map (shiftStringRight target stringEmp i) is == is } 
  / [llen is] @-}
mapShiftZero target i N
  =   map (shiftStringRight target stringEmp i) N ==. N *** QED  
mapShiftZero target i (C x xs)
  =   map (shiftStringRight target stringEmp i) (C x xs) 
  ==. shiftStringRight target stringEmp i x `C` map (shiftStringRight target stringEmp i) xs
  ==. shift (stringLen stringEmp) x `C` map (shiftStringRight target stringEmp i) xs
  ==. shift 0 x `C` map (shiftStringRight target stringEmp i) xs
  ==. x `C` map (shiftStringRight target stringEmp i) xs
  ==. x `C` xs ? mapShiftZero target i xs 
  *** QED 


{-@ mapShiftIndex :: tg:SMTString -> xi:SMTString -> yi:SMTString -> zi:SMTString -> xs:List (GoodIndex yi tg)
  -> {map (shiftStringRight tg xi yi) xs == map (shiftStringRight tg xi (concatString yi zi)) xs} / [llen xs] @-}
mapShiftIndex :: SMTString -> SMTString -> SMTString -> SMTString -> List Int -> Proof
mapShiftIndex tg xi yi zi N 
  = map (shiftStringRight tg xi yi) N ==. N ==. map (shiftStringRight tg xi (concatString yi zi)) N *** QED 
  *** QED 
mapShiftIndex tg xi yi zi zs@(C i0 is0)
  =   let is = castGoodIndexRightList tg yi zi is0 
          i  = castGoodIndexRight     tg yi zi i0  in 
      map (shiftStringRight tg xi yi) (C i is) 
  ==. C (shiftStringRight tg xi yi i) (map (shiftStringRight tg xi yi) is)
  ==. C (shift (stringLen xi) i) (map (shiftStringRight tg xi yi) is)
  ==. C (shiftStringRight tg xi (concatString yi zi) i) (map (shiftStringRight tg xi yi) is)
  ==. C (shiftStringRight tg xi (concatString yi zi) i) (map (shiftStringRight tg xi (concatString yi zi)) is)
       ? mapShiftIndex tg xi yi zi is
  ==. map (shiftStringRight tg xi (concatString yi zi)) (C i is)
  *** QED 



{-@ shiftNewIndices
  :: xi:SMTString 
  -> yi:SMTString 
  -> zi:SMTString 
  -> tg:{SMTString | stringLen yi < stringLen tg  } 
  -> {  append (makeNewIndices xi (concatString yi zi) tg) (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)) == append (castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)) (makeNewIndices (concatString xi yi) zi tg)
     }
  @-}
shiftNewIndices :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
shiftNewIndices xi yi zi tg 
  | stringLen tg < 2 
  =   append (makeNewIndices xi (concatString yi zi) tg) (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)) 
  ==. append N (map (shiftStringRight tg xi (concatString yi zi)) N) 
  ==. map (shiftStringRight tg xi (concatString yi zi)) N 
  ==. N 
  ==. append N N
  ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)) (makeNewIndices (concatString xi yi) zi tg)
  *** QED 

shiftNewIndices xi yi zi tg 
  | stringLen xi == 0 
  =   append (makeNewIndices xi (concatString yi zi) tg) 
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
  ==. append (makeNewIndices stringEmp (concatString yi zi) tg) 
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
  ? stringEmpProp xi 
  ==. append (makeNewIndices stringEmp (concatString yi zi) tg) 
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
  ? makeNewIndicesNullRight (concatString yi zi) tg
  ==. append N
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
  ==. map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)
       ? stringEmpProp xi
  ==. map (shiftStringRight tg stringEmp (concatString yi zi)) (makeNewIndices yi zi tg)
      ? mapShiftZero tg (concatString yi zi) (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
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)) (makeNewIndices (concatString xi yi) zi tg)
  *** QED 
  | stringLen yi == 0 
  =   append (makeNewIndices xi (concatString yi zi) tg) 
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
  ==. append (makeNewIndices xi zi tg) 
                  (map (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg))
      ? (stringEmpProp yi &&& concatEmpLeft yi zi)
  ==. append (makeNewIndices xi zi tg) 
                  (map (shiftStringRight tg xi zi) (makeNewIndices stringEmp zi tg))
  ==. append (makeNewIndices xi zi tg) 
                  (map (shiftStringRight tg xi (concatString stringEmp zi)) N)
      ? makeNewIndicesNullRight zi tg 
  ==. append (makeNewIndices xi zi tg) 
                  N
  ==. makeNewIndices xi zi tg 
       ? appendNil (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)
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (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 (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)) 
  ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                (maxInt (stringLen xi - stringLen tg + 1) 0)
                                (stringLen xi -1)) 
                  (map (shiftStringRight tg xi (concatString yi zi)) 
                            (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 (shiftStringRight tg xi (concatString yi zi)) 
                            (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 (shiftStringRight tg xi (concatString yi zi)) 
                            (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)) 
      ? mergeIndices (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)) 
      ? appendNil (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)
                  )
      ? catIndices (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)
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)) (makeNewIndices (concatString xi yi) zi tg)
  *** QED 
shiftNewIndices 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 (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)) 
  ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                (maxInt (stringLen xi - stringLen tg + 1) 0)
                                (stringLen xi -1)) 
                  (map (shiftStringRight tg xi (concatString yi zi)) 
                            (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 (shiftStringRight tg xi (concatString yi zi)) 
                            (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)) 
      ? mergeIndices (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))
     ? mergeIndices (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)
                  )
      ? catIndices (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)
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (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 (shiftStringRight tg xi (concatString yi zi)) (makeNewIndices yi zi tg)) 
  ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                (maxInt (stringLen xi - stringLen tg + 1) 0)
                                (stringLen xi -1)) 
                  (map (shiftStringRight tg xi (concatString yi zi)) 
                            (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 (shiftStringRight tg xi (concatString yi zi)) 
                            (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)
      ? mergeIndices (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)
  ==. append (castGoodIndexRightList tg (concatString xi yi) zi (makeNewIndices xi yi tg)) (makeNewIndices (concatString xi yi) zi tg)
  *** 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  

maxIndices :: SMTString -> SMTString -> Int -> Int -> Proof 
{-@ maxIndices 
  :: input:SMTString -> target:SMTString -> lo:{Nat | stringLen input < lo + stringLen target} -> hi:Int
  -> {makeIndices input target lo hi = N}
  / [hi - lo ] @-}
maxIndices 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 
      ? maxIndices input target (lo+1) hi 
  *** QED 


mergeIndices :: SMTString -> SMTString -> Int -> Int -> Int -> Proof
{-@ mergeIndices 
  :: 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] @-}
mergeIndices 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)
       ? mergeIndices 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)
       ? mergeIndices 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 


catIndices :: SMTString -> SMTString -> SMTString -> Int -> Int -> Proof 
{-@ catIndices 
     :: 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) }
  @-}
catIndices 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)
       ? mergeIndices input target lo (stringLen input - stringLen target) hi
  ==. append (makeIndices input target lo (stringLen input - stringLen target))
                  N
       ? maxIndices input target (stringLen input - stringLen target + 1) hi
  ==. makeIndices input target lo (stringLen input - stringLen target)
       ? appendNil (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