val nt_subst_comp (c: comp) (ss: nt_substs) : comp
let nt_subst_comp (c:comp) (ss:nt_substs) : comp =
  L.fold_left (fun c elt -> subst_comp c [elt]) c ss
val nt_subst_comp (c: comp) (ss: nt_substs) : comp
let nt_subst_comp (c: comp) (ss: nt_substs) : comp =
L.fold_left (fun c elt -> subst_comp c [elt]) c ss
Pulse.Checker.Prover.Substs.fsti.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Prover.Substs.fsti
Pulse.Syntax.Base.comp Pulse.Checker.Prover.Substs.nt_substs FStar.List.Tot.Base.fold_left Pulse.Syntax.Naming.subst_elt Pulse.Syntax.Naming.subst_comp Prims.Cons Prims.Nil
module Pulse.Checker.Prover.Substs

open FStar.List.Tot

open Pulse.Syntax
open Pulse.Typing.Env
open Pulse.Typing

module L = FStar.List.Tot
module T = FStar.Tactics

module Env = Pulse.Typing.Env

val ss_t : Type0

val as_map (ss:ss_t) : Map.t var term

let dom (ss:ss_t) = Map.domain (as_map ss)
let contains (ss:ss_t) (x:var) = Map.contains (as_map ss) x
let sel (ss:ss_t) (x:var { contains ss x }) = Map.sel (as_map ss) x

val empty : ss_t

val push (ss:ss_t) (x:var { ~ (contains ss x) }) (t:term) : ss_t

val push_ss (ss1:ss_t) (ss2:ss_t { Set.disjoint (dom ss1) (dom ss2) }) : ss_t

val check_disjoint (ss1 ss2:ss_t) : b:bool { b ==> Set.disjoint (dom ss1) (dom ss2) }

val push_as_map (ss1 ss2:ss_t)
  : Lemma (requires Set.disjoint (dom ss1) (dom ss2))
          (ensures as_map (push_ss ss1 ss2) == Map.concat (as_map ss1) (as_map ss2))
          [SMTPat (as_map (push_ss ss1 ss2))]

val ss_term (t:term) (ss:ss_t) : term
val ss_st_term (t:st_term) (ss:ss_t) : st_term
val ss_st_comp (s:st_comp) (ss:ss_t) : st_comp
val ss_comp (c:comp) (ss:ss_t) : comp
val ss_binder (b:binder) (ss:ss_t) : binder
val ss_env (g:env) (ss:ss_t)
  : g':env { fstar_env g' == fstar_env g /\
             Env.dom g' == Env.dom g }

val ss_st_comp_commutes (s:st_comp) (ss:ss_t)
  : Lemma (ensures
             ss_st_comp s ss ==
             { s with res = ss_term s.res ss;
                      pre = ss_term s.pre ss;
                      post = ss_term s.post ss; })  // no shifting required
          [SMTPat (ss_st_comp s ss)]

val ss_comp_commutes (c:comp) (ss:ss_t)
  : Lemma (ensures
             (let r = ss_comp c ss in
              (C_Tot? c ==> r == C_Tot (ss_term (comp_res c) ss)) /\
              (C_ST? c ==> r == C_ST (ss_st_comp (st_comp_of_comp c) ss)) /\
              (C_STAtomic? c ==> r == C_STAtomic (ss_term (comp_inames c) ss)
                                                 (ss_st_comp (st_comp_of_comp c) ss)) /\
              (C_STGhost? c ==> r == C_STGhost (ss_term (comp_inames c) ss)
                                               (ss_st_comp (st_comp_of_comp c) ss))))
          [SMTPat (ss_comp c ss)]

type nt_substs = l:list subst_elt { forall elt. L.memP elt l ==> NT? elt }

let nt_subst_term (t:term) (ss:nt_substs) : term =
  L.fold_left (fun t elt -> subst_term t [elt]) t ss

let nt_subst_binder (b:binder) (ss:nt_substs) : binder =
  L.fold_left (fun b elt -> subst_binder b [elt]) b ss

let nt_subst_st_term (t:st_term) (ss:nt_substs) : st_term =
  L.fold_left (fun t elt -> subst_st_term t [elt]) t ss

let nt_subst_st_comp (s:st_comp) (ss:nt_substs) : st_comp =
  L.fold_left (fun s elt -> subst_st_comp s [elt]) s ss
val nt_subst_comp (c: comp) (ss: nt_substs) : comp
c: Pulse.Syntax.Base.comp -> ss: Pulse.Checker.Prover.Substs.nt_substs -> Pulse.Syntax.Base.comp