val statements_match_per_pc_relation
      (relation return_relation: relation_t pc_t pc_t)
      (statement1 statement2: Armada.Statement.t)
    : GTot ubool
val statements_match_per_pc_relation
      (relation return_relation: relation_t pc_t pc_t)
      (statement1 statement2: Armada.Statement.t)
    : GTot ubool
let statements_match_per_pc_relation
  (relation: relation_t pc_t pc_t)
  (return_relation: relation_t pc_t pc_t)
  (statement1: Armada.Statement.t)
  (statement2: Armada.Statement.t)
  : GTot ubool =
  match statement1 with
  | CreateThreadStatement method_id1 initial_pc1 bypassing_write_buffer1 optional_result1 parameter_var_ids1
                          parameter_expressions1 local_variable_initializers1 ->
      (match statement2 with
       | CreateThreadStatement method_id2 initial_pc2 bypassing_write_buffer2 optional_result2 parameter_var_ids2
                               parameter_expressions2 local_variable_initializers2 ->
              method_id1 = method_id2
           /\ relation initial_pc1 initial_pc2
           /\ bypassing_write_buffer1 = bypassing_write_buffer2
           /\ optional_result1 == optional_result2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
       | _ -> False)
  | MethodCallStatement method_id1 return_pc1 parameter_var_ids1 parameter_expressions1 local_variable_initializers1
                          stack_overflow1 ->
      (match statement2 with
       | MethodCallStatement method_id2 return_pc2 parameter_var_ids2 parameter_expressions2
                             local_variable_initializers2 stack_overflow2 ->
              method_id1 = method_id2
           /\ relation return_pc1 return_pc2
           /\ return_relation return_pc1 return_pc2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
           /\ stack_overflow1 = stack_overflow2
       | _ -> False)
  | _ -> statement2 == statement1
module Strategies.GlobalVars.Statement

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.GlobalVars
open Strategies.PCIndices
open Strategies.PCRelation
open Util.ImmutableArray
open Util.Relation
/
Util.Relation.fst.checked Util.ImmutableArray.fsti.checked Strategies.PCRelation.fst.checked Strategies.PCIndices.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Statement.fsti

    relation: Util.Relation.relation_t Armada.Base.pc_t Armada.Base.pc_t ->
    return_relation: Util.Relation.relation_t Armada.Base.pc_t Armada.Base.pc_t ->
    statement1: Armada.Statement.t ->
    statement2: Armada.Statement.t
  -> Prims.GTot Spec.Ubool.ubool
Util.Relation.relation_t Armada.Base.pc_t Armada.Statement.t Armada.Base.method_id_t Prims.bool FStar.Pervasives.Native.option Armada.Expression.expression_t Prims.list Armada.Base.var_id_t Armada.Init.initializer_t Prims.l_and Prims.b2t Prims.op_Equality Prims.eq2 Prims.l_False Spec.Ubool.ubool
let statements_match_per_pc_relation
      (relation return_relation: relation_t pc_t pc_t)
      (statement1 statement2: Armada.Statement.t)
    : GTot ubool =
  
match statement1 with
| CreateThreadStatement
  method_id1
  initial_pc1
  bypassing_write_buffer1
  optional_result1
  parameter_var_ids1
  parameter_expressions1
  local_variable_initializers1 ->
  (match statement2 with
    | CreateThreadStatement
      method_id2
      initial_pc2
      bypassing_write_buffer2
      optional_result2
      parameter_var_ids2
      parameter_expressions2
      local_variable_initializers2 ->
      method_id1 = method_id2 /\ relation initial_pc1 initial_pc2 /\
      bypassing_write_buffer1 = bypassing_write_buffer2 /\ optional_result1 == optional_result2 /\
      parameter_var_ids1 = parameter_var_ids2 /\ parameter_expressions1 == parameter_expressions2 /\
      local_variable_initializers1 == local_variable_initializers2
    | _ -> False)
| MethodCallStatement
  method_id1
  return_pc1
  parameter_var_ids1
  parameter_expressions1
  local_variable_initializers1
  stack_overflow1 ->
  (match statement2 with
    | MethodCallStatement
      method_id2
      return_pc2
      parameter_var_ids2
      parameter_expressions2
      local_variable_initializers2
      stack_overflow2 ->
      method_id1 = method_id2 /\ relation return_pc1 return_pc2 /\
      return_relation return_pc1 return_pc2 /\ parameter_var_ids1 = parameter_var_ids2 /\
      parameter_expressions1 == parameter_expressions2 /\
      local_variable_initializers1 == local_variable_initializers2 /\
      stack_overflow1 = stack_overflow2
    | _ -> False)
| _ -> statement2 == statement1