// Add `decreases` clauses with single expressions to the below definitions
// so that the termination checker is happy.

function MergeLists(xs: List<int>, ys: List<int>): List<int>
{
  match (xs, ys)
  case (Nil, _) => ys
  case (_, Nil) => xs
  case (Cons(x, xs'), Cons(y, ys')) =>
    if x <= y then
      Cons(x, MergeLists(xs', ys))
    else
      Cons(y, MergeLists(xs, ys'))
}

function MergeSequences(a: seq<int>, b: seq<int>): seq<int>
{
  if a == [] then
    b
  else if b == [] then
    a
  else if a[0] <= b[0] then
    [a[0]] + MergeSequences(a[1..], b)
  else
    [b[0]] + MergeSequences(a, b[1..])
}

function MergeSequencesFrom(a: seq<int>, b: seq<int>, i: nat, j: nat): seq<int>
  requires i <= |a| && j <= |b|
{
  if i == |a| then
    b[j..]
  else if j == |b| then
    a[i..]
  else if a[i] <= b[j] then
    [a[i]] + MergeSequencesFrom(a, b, i + 1, j)
  else
    [b[j]] + MergeSequencesFrom(a, b, i, j + 1)
}

// Standard list definitions

datatype List<X> = Nil | Cons(head: X, tail: List<X>)

function Length<X>(xs: List<X>): nat
  decreases xs
{
  match xs
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}