-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.SortHelpers
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Various definitions and lemmas that are useful for sorting related proofs.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.SortHelpers where

import Prelude hiding (null, tail, elem, head, (++), take, drop)

import Data.SBV
import Data.SBV.List
import Data.SBV.TP
import Data.SBV.TP.List

#ifdef DOCTEST
-- $setup
-- >>> :set -XTypeApplications
-- >>> import Data.SBV.TP
#endif

-- | A predicate testing whether a given list is non-decreasing.
nonDecreasing :: (Ord a, SymVal a) => SList a -> SBool
nonDecreasing :: forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing = String -> (SList a -> SBool) -> SList a -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"nonDecreasing" ((SList a -> SBool) -> SList a -> SBool)
-> (SList a -> SBool) -> SList a -> SBool
forall a b. (a -> b) -> a -> b
$ \SList a
l ->  SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l SBool -> SBool -> SBool
.|| SList a -> SBool
forall a. SymVal a => SList a -> SBool
null (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
l)
                                                 SBool -> SBool -> SBool
.|| let (SBV a
x, SList a
l') = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l
                                                         (SBV a
y, SList a
_)  = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l'
                                                     in SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y SBool -> SBool -> SBool
.&& SList a -> SBool
forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing SList a
l'

-- | Are two lists permutations of each other?
isPermutation :: SymVal a => SList a -> SList a -> SBool
isPermutation :: forall a. SymVal a => SList a -> SList a -> SBool
isPermutation SList a
xs SList a
ys = (Forall "x" a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"x" SBV a
x) -> SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
count SBV a
x SList a
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
count SBV a
x SList a
ys)

-- | The tail of a non-decreasing list is non-decreasing. We have:
--
-- >>> runTP $ nonDecrTail @Integer
-- Lemma: nonDecrTail                      Q.E.D.
-- [Proven] nonDecrTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
nonDecrTail :: forall a. (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrTail :: forall a.
(Ord a, SymVal a) =>
TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrTail = String
-> (Forall "x" a -> Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"nonDecrTail"
                    (\(Forall SBV a
x) (Forall SBV [a]
xs) -> SBV [a] -> SBool
forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs) SBool -> SBool -> SBool
.=> SBV [a] -> SBool
forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing SBV [a]
xs)
                    []

-- | If we insert an element that is less than the head of a nonDecreasing list, it remains nondecreasing. We have:
--
-- >>> runTP $ nonDecrIns @Integer
-- Lemma: nonDecrInsert                    Q.E.D.
-- [Proven] nonDecrInsert :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
nonDecrIns :: forall a. (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrIns :: forall a.
(Ord a, SymVal a) =>
TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrIns = String
-> (Forall "x" a -> Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"nonDecrInsert"
                   (\(Forall SBV a
x) (Forall SBV [a]
xs) -> SBV [a] -> SBool
forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing SBV [a]
xs SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SBV [a] -> SBool
forall a. SymVal a => SList a -> SBool
null SBV [a]
xs) SBool -> SBool -> SBool
.&& SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV [a] -> SBV a
forall a. SymVal a => SList a -> SBV a
head SBV [a]
xs SBool -> SBool -> SBool
.=> SBV [a] -> SBool
forall a. (Ord a, SymVal a) => SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs))
                   []

-- | Sublist relationship
sublist :: SymVal a => SList a -> SList a -> SBool
sublist :: forall a. SymVal a => SList a -> SList a -> SBool
sublist SList a
xs SList a
ys = (Forall "e" a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"e" SBV a
e) -> SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
count SBV a
e SList a
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
count SBV a
e SList a
ys SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0)

-- | 'sublist' correctness. We have:
--
-- >>> runTP $ sublistCorrect @Integer
-- Inductive lemma: countNonNeg
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: countElem
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: elemCount
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: sublistCorrect
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] sublistCorrect :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐx ∷ Integer → Bool
sublistCorrect :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
sublistCorrect :: forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
sublistCorrect = do

    Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
cElem  <- forall a.
(Eq a, SymVal a) =>
TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
countElem @a
    Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
eCount <- forall a.
(Eq a, SymVal a) =>
TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
elemCount @a

    String
-> (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool) Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool) t
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"sublistCorrect"
         (\(Forall SBV [a]
xs) (Forall SBV [a]
ys) (Forall SBV a
x) -> SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys SBool -> SBool -> SBool
.&& SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
xs SBool -> SBool -> SBool
.=> SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
ys) (StepArgs
   (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool) Bool
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)))
-> StepArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool) Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
forall a b. (a -> b) -> a -> b
$
         \SBV [a]
xs SBV [a]
ys SBV a
x -> [SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys, SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
xs]
                  [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
ys
                  SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
cElem  Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "e" a -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SBV [a]
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
x)
                  TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
eCount Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "e" a -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SBV [a]
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
x)
                  Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

-- | If one list is a sublist of another, then its head is an elem. We have:
--
-- >>> runTP $ sublistElem @Integer
-- Inductive lemma: countNonNeg
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: countElem
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Inductive lemma: elemCount
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: sublistCorrect
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: sublistElem
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] sublistElem :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistElem :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistElem :: forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistElem = do
   Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
slc <- forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
sublistCorrect @a

   String
-> (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool
-> TP
     (Proof
        (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool) t
-> TP
     (Proof
        (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"sublistElem"
        (\(Forall SBV a
x) (Forall SBV [a]
xs) (Forall SBV [a]
ys) -> (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs) SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys SBool -> SBool -> SBool
.=> SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
ys) (StepArgs
   (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool
 -> TP
      (Proof
         (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)))
-> StepArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool
-> TP
     (Proof
        (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV a
x SBV [a]
xs SBV [a]
ys -> [(SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs) SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys]
                 [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a
x SBV a -> SBV [a] -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV [a]
ys
                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
slc Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SBV [a]
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x)
                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

-- | If one list is a sublist of another so is its tail. We have:
--
-- >>> runTP $ sublistTail @Integer
-- Lemma: sublistTail                      Q.E.D.
-- [Proven] sublistTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistTail :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistTail :: forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistTail =
  String
-> (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"sublistTail"
        (\(Forall SBV a
x) (Forall SBV [a]
xs) (Forall SBV [a]
ys) -> (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs) SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys SBool -> SBool -> SBool
.=> SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys)
        []

-- | Permutation implies sublist. We have:
--
-- >>> runTP $ sublistIfPerm @Integer
-- Lemma: sublistIfPerm                    Q.E.D.
-- [Proven] sublistIfPerm :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistIfPerm :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistIfPerm :: forall a.
(Eq a, SymVal a) =>
TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistIfPerm = String
-> (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"sublistIfPerm"
                      (\(Forall SBV [a]
xs) (Forall SBV [a]
ys) -> SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
isPermutation SBV [a]
xs SBV [a]
ys SBool -> SBool -> SBool
.=> SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`sublist` SBV [a]
ys)
                      []