// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

datatype list<A> = Nil | Cons(head: A, tail: list<A>)
datatype d = A | B(ds: list<d>)
datatype d2 = A2 | B2(ds: seq<d2>)
datatype d3 = A3 | B3(ds: set<d3>)

function d_size(x: d): int
{
  match x
  case A => 1
  case B(ds) => 1+ds_size(ds)
}

function ds_size(xs: list<d>): int
{
  match xs
  case Nil => 1
  case Cons(head, tail) => d_size(head)+ds_size(tail)
}

function d2_size(x: d2): int
{
  match x
  case A2 => 1
  case B2(ds) => 1+ds2_size(ds)
}

function ds2_size(xs: seq<d2>): int
{
  if (|xs|==0) then 1 else 1+d2_size(xs[0])+ds2_size(xs[1..])
}

function seq_dec_drop(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  1+seq_dec_drop(xs[1..])
}

function seq_dec_take(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  1+seq_dec_take(xs[..|xs|-1])
}

function seq_dec(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 < i <= |xs|;
  i+seq_dec(xs[i..])
}

function seq_dec'(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec'(xs[..i])
}

function seq_dec''(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  assert xs[0..i] == xs[..i];
  i+seq_dec''(xs[0..i])
}

function seq_dec'''(xs: seq<int>): int
  decreases |xs|;
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec'''(xs[..i]+xs[i+1..])
}

function seq_dec''''(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec''''(xs[..i]+xs[i+1..])
}