# Abstract Refinements

```5: module AbstractRefinements where
6:
7: import Prelude hiding (max)
9: {-@ LIQUID "--no-termination" @-}
```

# Polymorphic Max Function

Consinder a polymorphic max function:
```15: max     :: a -> a -> a
16: max x y = if x >= y then x else y
```

We can instantiate `a` with `Odd`
```22: max     :: Odd -> Odd -> Odd
23:
24: maxOdd :: Odd
25: maxOdd = max 3 7
```

In Haskell the type of max is
```32: max     :: Ord a => a -> a -> a
```

We could ignore the class constraints, and procced as before:

Instantiate `a` with `Odd`
```41: max     :: Odd -> Odd -> Odd
42:
43: maxOdd :: Odd
44: maxOdd = max 3 7
```

But this can lead to unsoundness:
```52: max     :: Ord a => a -> a -> a
53: (+)     :: Num a => a -> a -> a
```

So, ignoring class constraints allows us to: instantiate `a` with `Odd`
```60: (+)     :: Odd -> Odd -> Odd
61:
63: addOdd = 3 + 7
```

# Polymorphism via Parametric Invariants

`max` returns one of its two inputs `x` and `y`.

• If both inputs satisfy a property

• Then output must satisfy that property

This holds, regardless of what that property was!

• That is, we can abstract over refinements

• Or, parameterize a type over its refinements.

# Parametric Invariants

```86: {-@ max :: forall <p :: a -> Prop>. Ord a => a<p> -> a<p> -> a<p> @-}
87: max     :: Ord a => a -> a -> a
88: forall a <p :: a-> Bool>.
(GHC.Classes.Ord a) =>
{VV : a<p> | true} -> {VV : a<p> | true} -> {VV : a<p> | true}max {VV : a | ((papp1 p VV))}x {VV : a | ((papp1 p VV))}y = if {VV : a | ((papp1 p VV)) && (VV == x)}x x1:{VV : a | ((papp1 p VV))}
-> x2:{VV : a | ((papp1 p VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | ((papp1 p VV)) && (VV == y)}y then {VV : a | ((papp1 p VV)) && (VV == y)}y else {VV : a | ((papp1 p VV)) && (VV == x)}x
```

Where

• `a<p>` is just an abbreviation for `{v:a | (p v)}`

This type states explicitly:

• For any property `p`, that is a property of `a`,

• `max` takes two inputs of which satisfy `p`,

• `max` returns an output that satisfies `p`.

# Using Abstract Refinements

• If we call `max` with two arguments with the same concrete refinement,

• Then the `p` will be instantiated with that concrete refinement,

• The output of the call will also enjoy the concrete refinement.

```120: {-@ type Odd = {v:Int | (v mod 2) = 1} @-}
121:
122: {-@ maxOdd :: Odd @-}
123: maxOdd     :: Int
124: {VV : (GHC.Types.Int) | ((VV mod 2) == 1)}maxOdd     = {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 1) && (VV > 0)}max {VV : (GHC.Types.Int) | (VV == (3  :  int))}3 {VV : (GHC.Types.Int) | (VV == (5  :  int))}5
```

# Abstract Refinements in Type Constructors

Types cannot track information of monomorphic arguments:

```134: data F = F {{VV : (AbstractRefinements.F) | false}
-> {VV : (GHC.Types.Int) | false}w::Int}
```

The type `F` cannot give us information about the field `x`.

```142: forall a. {VV : a | false} -> {VV : a | false}foo = let (AbstractRefinements.F)f = (GHC.Types.Int) -> (AbstractRefinements.F)F {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 in -- :: f :: F
143:       case {VV : (AbstractRefinements.F) | (VV == f)}f of
144:       F x -> {VV : (GHC.Types.Bool) | ((Prop VV))}
-> {VV : a | false} -> {VV : a | false}liquidAssert ({VV : (GHC.Types.Int) | (VV == x)}x x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)
```

# Abstract Refinements in Type Constructors

• Abstract over the refinement you care
```152: data G = G {{VV : (AbstractRefinements.G <false>) | false}
-> {VV : (GHC.Types.Int) | false}y::Int{- <p> -}}
```
• Move it to the left-hand side
```157: {-@ data G <p :: Int -> Prop> = G (y::Int<p>) @-}
```
• The type `G <p>` now describes the field `x`.
```163: forall a. {VV : a | false} -> {VV : a | false}bar = let (AbstractRefinements.G <(VV == 0) && (VV /= AbstractRefinements.maxOdd)>)f = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true} -> (AbstractRefinements.G <p>)G {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 in -- :: f :: G <{v = 0}>
164:       case {VV : (AbstractRefinements.G <(VV == 0) && (VV /= AbstractRefinements.maxOdd)>) | (VV == f)}f of
165:       G x -> {VV : (GHC.Types.Bool) | ((Prop VV))}
-> {VV : a | false} -> {VV : a | false}liquidAssert ({VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}x x1:{VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}
-> x2:{VV : (GHC.Types.Int) | (VV == 0) && (VV == x) && (VV /= AbstractRefinements.maxOdd)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)
```

# Abstract Refinements in Lists

Remember increasing Lists?
```172: data IL a = N | C (x :: a) (xs :: L {v:a | x <= v})
```
• Abstract over the refinement you care
```177: data L a = N | C {forall a.
{VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}
-> {VV : a | false}x :: a, forall a.
{VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}
-> {VV : (AbstractRefinements.L <\_ VV -> false> {VV : a | false}) | false}xs :: L a {- v:a | p v x -}}
```
• Move it to the left-hand side
```182: {-@ data L a <p :: a -> a -> Prop> =
183:       N
184:     | C (x :: a) (xs :: L <p> a<p x>)  @-}
```

We can get back increasing Lists:

```191: {-@ type IncrL a = L <{\x v -> x <= v}> a @-}
```

# Multiple Instantiations

Now increasing lists
```199: type IncrL a = L <{\x v -> x <= v}> a
```

Co-exist with decreasing ones
```205: type DecrL a = L <{\x v -> x >= v}> a
```

# Ghc Sort

We can now verify algorithms that use both increasing and decreasing lists

```214: {-@ type OList a = [a]<{\hd v -> hd <= v}> @-}
215:
216: {-@ sort :: (Ord a) => [a] -> OList a  @-}
217: sort :: (Ord a) => [a] -> [a]
218: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\hd9 VV -> (hd9 <= VV)>sort = {VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll forall <q :: [a]-> [[a]]-> Bool, p :: [[a]]-> [a]-> Bool>.
(x:{VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}
-> {VV : [a]<\x4 VV -> (VV >= x4)><p x> | ((len VV) >= 0)})
-> (y:[a]
-> {VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)><q y> | ((len VV) > 0)})
-> x3:[a]
-> exists [z:{VV : [{VV : [a]<\x5 VV -> (VV >= x5)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)><q x3> | ((len VV) > 0)}].{VV : [a]<\x4 VV -> (VV >= x4)><p z> | ((len VV) >= 0)}. [a]
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences
219:   where
220:     [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences (a:b:xs)
221:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(GHC.Types.Ordering)
-> x2:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b {VV : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}a]  {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
222:       | otherwise           = x1:a
-> (x3:{VV : [{VV : a | (x1 <= VV)}]<\x3 VV -> (VV >= x3) && (VV >= x1)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending  {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:) {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
223:     sequences [x] = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}x]]
224:     sequences []  = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[]]
225:
226:     x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending aa {VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | ((len VV) > 0)}as (b:bs)
227:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(GHC.Types.Ordering)
-> x2:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b) && (VV >= a)}
-> x2:[{VV : a<p x1> | (VV > b) && (VV >= a)}]<p>
-> {VV : [{VV : a | (VV > b) && (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:{VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | (VV == as) && ((len VV) > 0) && ((len VV) >= 0)}as) {VV : [a] | (VV == bs) && ((len VV) >= 0)}bs
228:     descending a as bs      = ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:{VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | (VV == as) && ((len VV) > 0) && ((len VV) >= 0)}as)forall <p :: [a]-> [a]-> Bool>.
x1:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x2:[{VV : [a]<\x3 VV -> (VV >= x3)><p x1> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {VV : [a] | ((len VV) >= 0)}bs
229:
230:     x1:a
-> (x3:{VV : [{VV : a | (x1 <= VV)}]<\x3 VV -> (VV >= x3) && (VV >= x1)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending aa x1:{VV : [{VV : a | (a <= VV)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as (b:bs)
231:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(GHC.Types.Ordering)
-> x2:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 /= x2))}/= {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = x1:a
-> (x3:{VV : [{VV : a | (x1 <= VV)}]<\x3 VV -> (VV >= x3) && (VV >= x1)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (VV >= x2)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending {VV : a | (VV == b)}b (ys:{VV : [{VV : a | (a <= VV) && (b <= VV)}]<\x2 VV -> (VV >= a) && (VV >= b) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= ys) && ((len VV) > 0) && ((len VV) > (len ys))}\{VV : [{VV : a | (a <= VV) && (b <= VV)}]<\x1 VV -> (VV >= a) && (VV >= b) && (VV >= x1)> | ((len VV) > 0)}ys -> x1:{VV : [{VV : a | (a <= VV)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {VV : [{VV : a | (a <= VV)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:{VV : [{VV : a | (a <= VV) && (b <= VV)}]<\x1 VV -> (VV >= a) && (VV >= b) && (VV >= x1)> | (VV == ys) && ((len VV) > 0) && ((len VV) >= 0)}ys)) {VV : [a] | (VV == bs) && ((len VV) >= 0)}bs
232:     ascending a as bs       = x1:{VV : [{VV : a | (a <= VV)}]<\x2 VV -> (VV >= a) && (VV >= x2)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as {VV : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : a | (VV == a)}a]forall <p :: [a]-> [a]-> Bool>.
x1:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x2:[{VV : [a]<\x3 VV -> (VV >= x3)><p x1> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {VV : [a] | ((len VV) >= 0)}bs
```

# Ghc Sort : Helper Functions

```239: forall a.
(GHC.Classes.Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll [x] = {VV : [a]<\x1 VV -> (VV >= x1)> | (VV == x) && ((len VV) >= 0)}x
240: mergeAll xs  = forall a.
(GHC.Classes.Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}mergeAll (x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}xs)
241:
242: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x2))}mergePairs (a:b:xs) = x1:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x2:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len x2))}merge1 {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV == a) && ((len VV) >= 0)}a {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV == b) && ((len VV) >= 0)}bforall <p :: [a]-> [a]-> Bool>.
x1:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x2:[{VV : [a]<\x3 VV -> (VV >= x3)><p x1> | ((len VV) >= 0)}]<p>
-> {VV : [{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x2))}mergePairs {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | (VV == xs) && ((len VV) >= 0)}xs
243: mergePairs [x]      = {VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}[{VV : [a]<\x1 VV -> (x1 <= VV)> | (VV == a) && ((len VV) >= 0)}x]
244: mergePairs []       = forall <p :: [a]-> [a]-> Bool>.
{VV : [{VV : [{VV : a | false}]<\_ VV -> false> | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0)}[]
245:
246: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 (a:as') (b:bs')
247:   | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(GHC.Types.Ordering)
-> x2:(GHC.Types.Ordering)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {VV : (GHC.Types.Ordering) | (VV == GHC.Types.GT) && ((cmp VV) == GHC.Types.GT)}GT = {VV : a | (VV == b)}bforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= b)}
-> x2:[{VV : a<p x1> | (VV >= b)}]<p>
-> {VV : [{VV : a | (VV >= b)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b) && (VV >= a)}
-> x2:[{VV : a<p x1> | (VV > b) && (VV >= a)}]<p>
-> {VV : [{VV : a | (VV > b) && (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:{VV : [{VV : a | (VV >= a)}]<\x1 VV -> (VV >= x1)> | (VV == as') && ((len VV) >= 0)}as')  {VV : [{VV : a | (b <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == bs') && ((len VV) >= 0)}bs'
248:   | otherwise           = {VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {VV : [{VV : a | (VV >= a)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 {VV : [{VV : a | (VV >= a)}]<\x1 VV -> (VV >= x1)> | (VV == as') && ((len VV) >= 0)}as' ({VV : a | (VV == b)}bforall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV) && (b <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV) && (b <= VV)}]<p>
-> {VV : [{VV : a | (a <= VV) && (b <= VV)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}:{VV : [{VV : a | (b <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == bs') && ((len VV) >= 0)}bs')
249: merge1 [] bs            = {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}bs
250: merge1 as []            = {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}as
```