val compare_lseq' (#a: eqtype) (f: cmp a) (l: nat) (s1 s2: Seq.lseq a l) : Tot bool
val compare_lseq' (#a: eqtype) (f: cmp a) (l: nat) (s1 s2: Seq.lseq a l) : Tot bool
let rec compare_lseq' (#a:eqtype) (f:cmp a) (l:nat) (s1 s2:Seq.lseq a l)
  : Tot bool
  = if l = 0 then (assert (Seq.equal s1 s2); true)
    else if s1 = s2 then true
    else if Seq.head s1 = Seq.head s2 then compare_lseq' f (l - 1) (Seq.tail s1) (Seq.tail s2)
    else f (Seq.head s1) (Seq.head s2)
module Zeta.MultiSetHashDomain

module K = Zeta.Key
module R = Zeta.Record
module M = Zeta.Merkle

let nkey (n:nat) = k:base_key{Zeta.BinTree.depth k = n}

let rec compare_nkey (n:nat)
  : cmp (nkey n)
  = let open Zeta.BinTree in
    let f =
        fun (k1 k2:nkey n) ->
          match k1, k2 with
          | Root, Root -> true
          | LeftChild _, RightChild _ -> true
          | RightChild _, LeftChild _ -> false
          | LeftChild c1, LeftChild c2
          | RightChild c1, RightChild c2  -> compare_nkey (n - 1) c1 c2
    in
    f

let compare_key
  : cmp base_key
  = let f = fun (k1 k2:base_key) ->
        let open Zeta.BinTree in
        if k1 = k2 then true
        else if depth k1 = depth k2 then compare_nkey (depth k1) k1 k2
        else depth k1 <= depth k2
    in
    f

let compare_merkle_key
  : cmp merkle_key
  = let f = fun (k1 k2:merkle_key) ->
        let open Zeta.BinTree in
        if k1 = k2 then true
        else if depth k1 = depth k2 then compare_nkey (depth k1) k1 k2
        else depth k1 <= depth k2
    in
    f
/
Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Hash.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.MultiSetHashDomain.fst

    f: Zeta.MultiSet.cmp a ->
    l: Prims.nat ->
    s1: FStar.Seq.Properties.lseq a l ->
    s2: FStar.Seq.Properties.lseq a l
  -> Prims.bool
Prims.eqtype Zeta.MultiSet.cmp Prims.nat FStar.Seq.Properties.lseq Prims.op_Equality Prims.int Prims.unit Prims._assert FStar.Seq.Base.equal Prims.bool FStar.Seq.Properties.head Zeta.MultiSetHashDomain.compare_lseq' Prims.op_Subtraction FStar.Seq.Properties.tail
let rec compare_lseq' (#a: eqtype) (f: cmp a) (l: nat) (s1 s2: Seq.lseq a l) : Tot bool =
  
if l = 0
then
  (assert (Seq.equal s1 s2);
    true)
else
  if s1 = s2
  then true
  else
    if Seq.head s1 = Seq.head s2
    then compare_lseq' f (l - 1) (Seq.tail s1) (Seq.tail s2)
    else f (Seq.head s1) (Seq.head s2)