val split3_index (#a: eqtype) (s0: seq a) (x: a) (s1: seq a) (j: nat)
    : Lemma (requires j < Seq.length (Seq.append s0 s1))
      (ensures
        (let s = Seq.append s0 (Seq.cons x s1) in
          let s' = Seq.append s0 s1 in
          let n = Seq.length s0 in
          if j < n then Seq.index s' j == Seq.index s j else Seq.index s' j == Seq.index s (j + 1)))
let split3_index (#a:eqtype) (s0:seq a) (x:a) (s1:seq a) (j:nat)
  : Lemma
    (requires j < Seq.length (Seq.append s0 s1))
    (ensures (
      let s = Seq.append s0 (Seq.cons x s1) in
      let s' = Seq.append s0 s1 in
      let n = Seq.length s0 in
      if j < n then Seq.index s' j == Seq.index s j
      else Seq.index s' j == Seq.index s (j + 1)
    ))
  = let n = Seq.length (Seq.append s0 s1) in
    if j < n then ()
    else ()
val split3_index (#a: eqtype) (s0: seq a) (x: a) (s1: seq a) (j: nat)
    : Lemma (requires j < Seq.length (Seq.append s0 s1))
      (ensures
        (let s = Seq.append s0 (Seq.cons x s1) in
          let s' = Seq.append s0 s1 in
          let n = Seq.length s0 in
          if j < n then Seq.index s' j == Seq.index s j else Seq.index s' j == Seq.index s (j + 1)))
let split3_index (#a: eqtype) (s0: seq a) (x: a) (s1: seq a) (j: nat)
    : Lemma (requires j < Seq.length (Seq.append s0 s1))
      (ensures
        (let s = Seq.append s0 (Seq.cons x s1) in
          let s' = Seq.append s0 s1 in
          let n = Seq.length s0 in
          if j < n then Seq.index s' j == Seq.index s j else Seq.index s' j == Seq.index s (j + 1))) =
let n = Seq.length (Seq.append s0 s1) in
if j < n then ()
FStar.Seq.Permutation.fst.checked
prims.fst.checked FStar.Seq.Equiv.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Seq.Permutation.fst
Prims.eqtype FStar.Seq.Base.seq Prims.nat Prims.op_LessThan Prims.bool Prims.unit FStar.Seq.Base.length FStar.Seq.Base.append Prims.b2t Prims.squash Prims.eq2 FStar.Seq.Base.index Prims.op_Addition FStar.Seq.Properties.cons Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2021-2022 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Authors: N. Swamy, A. Rastogi, A. Rozanov
*)
module FStar.Seq.Permutation
open FStar.Seq
open FStar.Calc

[@@"opaque_to_smt"]
let is_permutation (#a:Type) (s0:seq a) (s1:seq a) (f:index_fun s0) =
  Seq.length s0 == Seq.length s1 /\
  (forall x y. // {:pattern f x; f y}
  x <> y ==> f x <> f y) /\
  (forall (i:nat{i < Seq.length s0}). // {:pattern (Seq.index s1 (f i))}
      Seq.index s0 i == Seq.index s1 (f i))

let reveal_is_permutation #a (s0 s1:seq a) (f:index_fun s0)
  = reveal_opaque (`%is_permutation) (is_permutation s0 s1 f)

let reveal_is_permutation_nopats (#a:Type) (s0 s1:seq a) (f:index_fun s0)
  : Lemma (is_permutation s0 s1 f <==>

           Seq.length s0 == Seq.length s1 /\

           (forall x y. x <> y ==> f x <> f y) /\

           (forall (i:nat{i < Seq.length s0}).
              Seq.index s0 i == Seq.index s1 (f i)))
   = reveal_is_permutation s0 s1 f

let split3_index (#a:eqtype) (s0:seq a) (x:a) (s1:seq a) (j:nat)
  : Lemma
    (requires j < Seq.length (Seq.append s0 s1))
    (ensures (
      let s = Seq.append s0 (Seq.cons x s1) in
      let s' = Seq.append s0 s1 in
      let n = Seq.length s0 in
      if j < n then Seq.index s' j == Seq.index s j
      else Seq.index s' j == Seq.index s (j + 1)
val split3_index (#a: eqtype) (s0: seq a) (x: a) (s1: seq a) (j: nat)
    : Lemma (requires j < Seq.length (Seq.append s0 s1))
      (ensures
        (let s = Seq.append s0 (Seq.cons x s1) in
          let s' = Seq.append s0 s1 in
          let n = Seq.length s0 in
          if j < n then Seq.index s' j == Seq.index s j else Seq.index s' j == Seq.index s (j + 1)))
s0: FStar.Seq.Base.seq a -> x: a -> s1: FStar.Seq.Base.seq a -> j: Prims.nat
  -> FStar.Pervasives.Lemma (requires j < FStar.Seq.Base.length (FStar.Seq.Base.append s0 s1))
      (ensures
        (let s = FStar.Seq.Base.append s0 (FStar.Seq.Properties.cons x s1) in
          let s' = FStar.Seq.Base.append s0 s1 in
          let n = FStar.Seq.Base.length s0 in
          (match j < n with
            | true -> FStar.Seq.Base.index s' j == FStar.Seq.Base.index s j
            | _ -> FStar.Seq.Base.index s' j == FStar.Seq.Base.index s (j + 1))
          <:
          Type0))