isInfixOf package:sbv

isInfixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool

isInfixOf sub l. Does l contain the subsequence sub?

>>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 ++ l2 ++ l3)
Q.E.D.

>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 .&& l2 `isInfixOf` l1 .<=> l1 .== l2
Q.E.D.

>>> prove $ \(s1 :: SString) s2 s3 -> s2 `isInfixOf` (s1 ++ s2 ++ s3)
Q.E.D.

>>> prove $ \(s1 :: SString) s2 -> s1 `isInfixOf` s2 .&& s2 `isInfixOf` s1 .<=> s1 .== s2
Q.E.D.