let internally_disjoint8 #len #a (b0 b1 b2 b3 b4 b5 b6 b7: lbuffer a len) =
  disjoint b0 b1 /\ disjoint b0 b2 /\ disjoint b0 b3 /\ disjoint b0 b4 /\ disjoint b0 b5 /\ disjoint b0 b6 /\ disjoint b0 b7 /\
  disjoint b1 b2 /\ disjoint b1 b3 /\ disjoint b1 b4 /\ disjoint b1 b5 /\ disjoint b1 b6 /\ disjoint b1 b7 /\
  disjoint b2 b3 /\ disjoint b2 b4 /\ disjoint b2 b5 /\ disjoint b2 b6 /\ disjoint b2 b7 /\
  disjoint b3 b4 /\ disjoint b3 b5 /\ disjoint b3 b6 /\ disjoint b3 b7 /\
  disjoint b4 b5 /\ disjoint b4 b6 /\ disjoint b4 b7 /\
  disjoint b5 b6 /\ disjoint b5 b7 /\
  disjoint b6 b7
let internally_disjoint8
      #len
      #a
      (b0: lbuffer a len)
      (b1: lbuffer a len)
      (b2: lbuffer a len)
      (b3: lbuffer a len)
      (b4: lbuffer a len)
      (b5: lbuffer a len)
      (b6: lbuffer a len)
      (b7: lbuffer a len)
     =
disjoint b0 b1 /\ disjoint b0 b2 /\ disjoint b0 b3 /\ disjoint b0 b4 /\ disjoint b0 b5 /\
disjoint b0 b6 /\ disjoint b0 b7 /\ disjoint b1 b2 /\ disjoint b1 b3 /\ disjoint b1 b4 /\
disjoint b1 b5 /\ disjoint b1 b6 /\ disjoint b1 b7 /\ disjoint b2 b3 /\ disjoint b2 b4 /\
disjoint b2 b5 /\ disjoint b2 b6 /\ disjoint b2 b7 /\ disjoint b3 b4 /\ disjoint b3 b5 /\
disjoint b3 b6 /\ disjoint b3 b7 /\ disjoint b4 b5 /\ disjoint b4 b6 /\ disjoint b4 b7 /\
disjoint b5 b6 /\ disjoint b5 b7 /\ disjoint b6 b7
Lib.MultiBuffer.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.NTuple.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Lib.MultiBuffer.fst
Lib.IntTypes.size_t Lib.Buffer.lbuffer Prims.l_and Lib.Buffer.disjoint Lib.Buffer.MUT Prims.logical
module Lib.MultiBuffer

open FStar.Mul
module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All

open Lib.IntTypes
open Lib.Sequence
open Lib.Buffer
open Lib.NTuple

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"

let live4 #a #len (h:mem) (b0 b1 b2 b3: lbuffer a len) =
  live h b0 /\ live h b1 /\ live h b2 /\ live h b3

let live8 #a #len (h:mem) (b0 b1 b2 b3 b4 b5 b6 b7: lbuffer a len) =
  live h b0 /\ live h b1 /\ live h b2 /\ live h b3 /\ live h b4 /\ live h b5 /\ live h b6 /\ live h b7

let internally_disjoint4 #len #a (b0 b1 b2 b3: lbuffer a len) =
  disjoint b0 b1 /\ disjoint b0 b2 /\ disjoint b0 b3 /\
  disjoint b1 b2 /\ disjoint b1 b3 /\ disjoint b2 b3
val internally_disjoint8 : b0: Lib.Buffer.lbuffer a len ->
    b1: Lib.Buffer.lbuffer a len ->
    b2: Lib.Buffer.lbuffer a len ->
    b3: Lib.Buffer.lbuffer a len ->
    b4: Lib.Buffer.lbuffer a len ->
    b5: Lib.Buffer.lbuffer a len ->
    b6: Lib.Buffer.lbuffer a len ->
    b7: Lib.Buffer.lbuffer a len
  -> Prims.logical

    b0: Lib.Buffer.lbuffer a len ->
    b1: Lib.Buffer.lbuffer a len ->
    b2: Lib.Buffer.lbuffer a len ->
    b3: Lib.Buffer.lbuffer a len ->
    b4: Lib.Buffer.lbuffer a len ->
    b5: Lib.Buffer.lbuffer a len ->
    b6: Lib.Buffer.lbuffer a len ->
    b7: Lib.Buffer.lbuffer a len
  -> Prims.logical