val pc_matches_pc_index (pcs: array_t pc_t) (pc: pc_t) (n: nat) : GTot bool
val pc_matches_pc_index (pcs: array_t pc_t) (pc: pc_t) (n: nat) : GTot bool
let pc_matches_pc_index
  (pcs: array_t pc_t)
  (pc: pc_t)
  (n: nat)
  : GTot bool =
  n < array_len pcs && pc = array_index pcs n
module Strategies.PCIndices

open Armada.Action
open Armada.Base
open Armada.Statement
open Spec.Ubool
open Util.ImmutableArray
open Util.List
open Util.Relation

type statement_pc_indices_t = {
  start_pc_index: option nat;
  end_pc_index: option nat;
  create_thread_initial_pc_index: option nat;
  method_call_return_pc_index: option nat;
}
/
Util.Relation.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Statement.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.PCIndices.fst
pcs: Util.ImmutableArray.array_t Armada.Base.pc_t -> pc: Armada.Base.pc_t -> n: Prims.nat
  -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.nat Prims.op_AmpAmp Prims.op_LessThan Util.ImmutableArray.array_len Prims.op_Equality Util.ImmutableArray.array_index Prims.bool
let pc_matches_pc_index (pcs: array_t pc_t) (pc: pc_t) (n: nat) : GTot bool =
  
n < array_len pcs && pc = array_index pcs n