val compare_lseq (#a: eqtype) (f: cmp a) (l: nat) : cmp (Seq.lseq a l)
val compare_lseq (#a: eqtype) (f: cmp a) (l: nat) : cmp (Seq.lseq a l)
let compare_lseq (#a:eqtype) (f:cmp a) (l:nat)
  : cmp (Seq.lseq a l)
  = compare_lseq'_total_order f l;
    compare_lseq' f l
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

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)

let rec compare_lseq'_total_order #a (c:cmp a) (l:nat)
  : Lemma (total_order (Seq.lseq a l) (compare_lseq' c l))
  = let f = compare_lseq' c l in
    if l = 0
    then (
      assert (forall (a1 a2: Seq.lseq a l). (f a1 a2 /\ f a2 a1)  ==> a1 `Seq.equal` a2 /\ a1 == a2)  (* anti-symmetry *)
    )
    else (
      let f' = compare_lseq' c (l - 1) in
      let aux (a1 a2:Seq.lseq a l)
        : Lemma
          (requires (Seq.head a1 = Seq.head a2))
          (ensures (f a1 a2 == f' (Seq.tail a1) (Seq.tail a2)))
          [SMTPat (f a1 a2)]
        = ()
      in
      compare_lseq'_total_order c (l - 1);
      assert (total_order _ f');
      let aux (s1 s2:Seq.lseq a l)
        : Lemma
          (requires
            Seq.head s1 == Seq.head s2 /\
            Seq.equal (Seq.tail s1) (Seq.tail s2))
          (ensures
            s1 == s2)
          [SMTPat (Seq.head s1);
           SMTPat (Seq.head s2)]
        =  assert (s1 `Seq.equal` Seq.cons (Seq.head s1) (Seq.tail s1));
           assert (s2 `Seq.equal` Seq.cons (Seq.head s2) (Seq.tail s2));
           assert (Seq.equal s1 s2)
      in
      assert (forall (a1 a2:Seq.lseq a l). (f a1 a2 /\ f a2 a1)  ==> a1 `Seq.equal` a2);   (* anti-symmetry *)
      assert (forall (a1 a2 a3:Seq.lseq a l). f a1 a2 /\ f a2 a3 ==> f a1 a3);    (* transitivity  *)
      assert (forall (a1 a2:Seq.lseq a l). f a1 a2 \/ f a2 a1)                    (* totality      *)
    )
/
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 -> Zeta.MultiSet.cmp (FStar.Seq.Properties.lseq a l)
Prims.eqtype Zeta.MultiSet.cmp Prims.nat Zeta.MultiSetHashDomain.compare_lseq' Prims.unit Zeta.MultiSetHashDomain.compare_lseq'_total_order FStar.Seq.Properties.lseq
let compare_lseq (#a: eqtype) (f: cmp a) (l: nat) : cmp (Seq.lseq a l) =
  
compare_lseq'_total_order f l;
compare_lseq' f l