val compare_merkle_key:cmp merkle_key
val compare_merkle_key:cmp merkle_key
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
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
/
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
Zeta.MultiSet.cmp Zeta.Key.merkle_key
Zeta.Key.merkle_key Prims.bool Prims.op_Equality Prims.nat Zeta.BinTree.depth Zeta.MultiSetHashDomain.compare_nkey Prims.op_LessThanOrEqual
let compare_merkle_key:cmp merkle_key =
  
let f =
  fun (k1: merkle_key) (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