val armada_atomic_substep_invariant_witness_valid
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
      (aiw: armada_atomic_substep_invariant_witness_t program inv)
    : GTot ubool
val armada_atomic_substep_invariant_witness_valid
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
      (aiw: armada_atomic_substep_invariant_witness_t program inv)
    : GTot ubool
let armada_atomic_substep_invariant_witness_valid
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t)
  (aiw: armada_atomic_substep_invariant_witness_t program inv)
  : GTot ubool =
  armada_atomic_substep_special_cases_apply inv aiw.action_pred program.actions aiw.special_case_proofs
module Strategies.Invariant.Armada.AtomicSubstep

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Invariant
open Strategies.Invariant.Armada
open Util.List

noeq type armada_atomic_substep_invariant_witness_t
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t) =
{
  action_pred: Armada.Action.t -> GTot ubool;
  special_case_proofs: list (list (option (armada_action_special_case_invariant_proof_t inv)));
  init_implies_inv_proof: (s: Armada.State.t{program.init_f s}) -> squash (inv s);
  action_proof: armada_action_maintains_invariant_proof_t inv action_pred;
}

let armada_atomic_substep_special_cases_apply
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool)
  (program_actions: list (list Armada.Action.t))
  (special_case_proofs: (list (list (option (armada_action_special_case_invariant_proof_t inv))))) =
  lists_correspond_ubool
    (lists_correspond_ubool (armada_action_proof_option_applies inv action_pred))
    program_actions
    special_case_proofs
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.fsti.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.AtomicSubstep.fsti

    program:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    aiw:
      Strategies.Invariant.Armada.AtomicSubstep.armada_atomic_substep_invariant_witness_t program
        inv
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.Invariant.invariant_t Armada.State.t Strategies.Invariant.Armada.AtomicSubstep.armada_atomic_substep_invariant_witness_t Strategies.Invariant.Armada.AtomicSubstep.armada_atomic_substep_special_cases_apply Strategies.Invariant.Armada.AtomicSubstep.__proj__Mkarmada_atomic_substep_invariant_witness_t__item__action_pred Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.Invariant.Armada.AtomicSubstep.__proj__Mkarmada_atomic_substep_invariant_witness_t__item__special_case_proofs Spec.Ubool.ubool
let armada_atomic_substep_invariant_witness_valid
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
      (aiw: armada_atomic_substep_invariant_witness_t program inv)
    : GTot ubool =
  
armada_atomic_substep_special_cases_apply inv
  aiw.action_pred
  program.actions
  aiw.special_case_proofs