val update_expressions_lacking_pointer_field_maintains_states_match
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (exps: list expression_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (bypassing_write_buffer: bool)
      (new_values: list object_value_t)
      (s1 s2: Armada.State.t)
    : Lemma
      (requires
        states_match_except_global_variables vs pc_relation s1 s2 /\
        global_variables_unaddressed_in_memory vs s1.mem /\
        global_variables_unaddressed_in_memory vs s2.mem /\ roots_match s1.mem /\ roots_match s2.mem /\
        ThreadStatusRunning? (s1.threads actor).status /\
        global_variables_unmentioned_in_expressions vs exps /\ expressions_lack_pointer_field exps)
      (ensures
        (match
            update_expressions exps
              actor
              writer_pc1
              writer_expression_number1
              bypassing_write_buffer
              new_values
              s1,
            update_expressions exps
              actor
              writer_pc2
              writer_expression_number2
              bypassing_write_buffer
              new_values
              s2
          with
          | ComputationProduces s1', ComputationProduces s2' ->
            states_match_except_global_variables vs pc_relation s1' s2' /\
            global_variables_unaddressed_in_memory vs s1'.mem /\
            global_variables_unaddressed_in_memory vs s2'.mem /\ roots_match s1'.mem /\
            roots_match s2'.mem /\ ThreadStatusRunning? (s1'.threads actor).status
          | ComputationImpossible, ComputationImpossible -> True
          | ComputationUndefined, ComputationUndefined -> True
          | _ -> False))
val update_expressions_lacking_pointer_field_maintains_states_match
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (exps: list expression_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (bypassing_write_buffer: bool)
      (new_values: list object_value_t)
      (s1 s2: Armada.State.t)
    : Lemma
      (requires
        states_match_except_global_variables vs pc_relation s1 s2 /\
        global_variables_unaddressed_in_memory vs s1.mem /\
        global_variables_unaddressed_in_memory vs s2.mem /\ roots_match s1.mem /\ roots_match s2.mem /\
        ThreadStatusRunning? (s1.threads actor).status /\
        global_variables_unmentioned_in_expressions vs exps /\ expressions_lack_pointer_field exps)
      (ensures
        (match
            update_expressions exps
              actor
              writer_pc1
              writer_expression_number1
              bypassing_write_buffer
              new_values
              s1,
            update_expressions exps
              actor
              writer_pc2
              writer_expression_number2
              bypassing_write_buffer
              new_values
              s2
          with
          | ComputationProduces s1', ComputationProduces s2' ->
            states_match_except_global_variables vs pc_relation s1' s2' /\
            global_variables_unaddressed_in_memory vs s1'.mem /\
            global_variables_unaddressed_in_memory vs s2'.mem /\ roots_match s1'.mem /\
            roots_match s2'.mem /\ ThreadStatusRunning? (s1'.threads actor).status
          | ComputationImpossible, ComputationImpossible -> True
          | ComputationUndefined, ComputationUndefined -> True
          | _ -> False))
let rec update_expressions_lacking_pointer_field_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expressions vs exps
                    /\ expressions_lack_pointer_field exps)
          (ensures  (match update_expressions exps actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_values s1,
                           update_expressions exps actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_values s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                         /\ ThreadStatusRunning? (s1'.threads actor).status
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_lacking_pointer_field_maintains_states_match vs pc_relation
        first_exp actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2
        bypassing_write_buffer first_new_value s1 s2;
      (match update_expression first_exp actor writer_pc1 writer_expression_number1
               bypassing_write_buffer first_new_value s1,
             update_expression first_exp actor writer_pc2 writer_expression_number2
               bypassing_write_buffer first_new_value s2 with
       | ComputationProduces s1_next, ComputationProduces s2_next ->
           update_expressions_lacking_pointer_field_maintains_states_match vs pc_relation
             remaining_exps actor writer_pc1 writer_pc2 (writer_expression_number1 + 1) (writer_expression_number2 + 1)
             bypassing_write_buffer remaining_new_values s1_next s2_next;
           (match update_expressions exps actor writer_pc1 writer_expression_number1
                    bypassing_write_buffer new_values s1,
                  update_expressions exps actor writer_pc2 writer_expression_number2
                    bypassing_write_buffer new_values s2 with
            | ComputationProduces s1', ComputationProduces s2' -> ()
            | ComputationImpossible, ComputationImpossible -> ()
            | ComputationUndefined, ComputationUndefined -> ()
            | _, _ -> ())
       | ComputationImpossible, ComputationImpossible -> ()
       | ComputationUndefined, ComputationUndefined -> ()
       | _, _ -> ())
  | _, _ -> ()
module Strategies.GlobalVars.Util

open Armada.Base
open Armada.BinaryOp
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Armada.UnaryOp
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Pointer
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Value
open Strategies.PCRelation
open Util.List
open Util.Nth
open Util.Seq
open Util.Trigger

let memories_match_except_global_variables_reflexive (vs: list var_id_t) (mem: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem mem) =
  ()

let memories_match_except_global_variables_commutative
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem1 mem2 <==>
             memories_match_except_global_variables vs mem2 mem1) =
  ()

let memories_match_except_global_variables_transitive
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  (mem3: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ memories_match_except_global_variables vs mem2 mem3)
          (ensures  memories_match_except_global_variables vs mem1 mem3) =
  introduce forall root_id. (match root_id with
                        | RootIdGlobal v -> list_contains v vs \/ (mem1 root_id == mem3 root_id)
                        | _ -> mem1 root_id == mem3 root_id)
  with (
    match root_id with
    | RootIdGlobal v ->
        assert (list_contains v vs \/ (mem1 root_id == mem2 root_id));
        assert (list_contains v vs \/ (mem2 root_id == mem3 root_id))
    | _ ->
        assert (mem1 root_id == mem2 root_id);
        assert (mem2 root_id == mem3 root_id)
  )

let equality_pc_relation_implies_state_matches_itself_except_global_variables
  (vs: list var_id_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  states_match_except_global_variables vs equality_pc_relation s s) =
  introduce forall tid. stacks_match_per_pc_relation equality_pc_relation (s.threads tid).stack (s.threads tid).stack
  with equality_pc_relation_implies_stack_matches_itself (s.threads tid).stack;
  assert (threads_match_except_write_buffers_per_pc_relation equality_pc_relation s.threads s.threads);
  introduce forall sender_tid receiver_tid.
              sender_receiver_trigger sender_tid receiver_tid ==>
              write_buffers_match_except_global_variables vs
                (unread_write_buffer s.threads sender_tid receiver_tid)
                (unread_write_buffer s.threads sender_tid receiver_tid)
  with introduce _ ==> _
  with _.
    equality_pc_relation_implies_write_buffer_matches_itself
      (remove_global_variables_from_write_buffer vs
        (seq_to_list (unread_write_buffer s.threads sender_tid receiver_tid)))

#push-options "--z3rlimit 60"

let update_expression_lacking_pointer_field_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expression vs exp
                    /\ object_td_lacks_pointer_field (expression_to_td exp))
          (ensures  (match update_expression exp actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_value s1,
                           update_expression exp actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_value s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    lvalue_computation_doesnt_depend_on_global_variables vs pc_relation exp actor s1 s2;
    assert (lvalue_computation exp actor s1 == lvalue_computation exp actor s2);
    let td = expression_to_td exp in
    match lvalue_computation exp actor s1 with
    | ComputationProduces p ->
        update_pointed_to_value_lacking_pointer_field_maintains_states_match vs pc_relation p actor
          writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2 bypassing_write_buffer
          td new_value s1 s2;
        (match update_pointed_to_value p actor writer_pc1 writer_expression_number1 bypassing_write_buffer
                 new_value s1,
               update_pointed_to_value p actor writer_pc2 writer_expression_number2 bypassing_write_buffer
                 new_value s2 with
         | ComputationProduces s1', ComputationProduces s2' -> ()
         | ComputationImpossible, ComputationImpossible -> ()
         | ComputationUndefined, ComputationUndefined -> ()
         | _, _ -> false_elim ())
    | _ -> ()
  )

#pop-options
#push-options "--z3rlimit 80"

let update_expression_with_gvars_unaddressed_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expression vs exp
                    /\ global_variables_unaddressed_in_object_value vs new_value)
          (ensures  (match update_expression exp actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_value s1,
                           update_expression exp actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_value s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    lvalue_computation_doesnt_depend_on_global_variables vs pc_relation exp actor s1 s2;
    assert (lvalue_computation exp actor s1 == lvalue_computation exp actor s2);
    let td = expression_to_td exp in
    match lvalue_computation exp actor s1 with
    | ComputationProduces p ->
        update_pointed_to_value_with_gvars_unaddressed_maintains_states_match vs pc_relation
          p actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2 bypassing_write_buffer
          new_value s1 s2;
        (match update_pointed_to_value p actor writer_pc1 writer_expression_number1 bypassing_write_buffer
                 new_value s1,
               update_pointed_to_value p actor writer_pc2 writer_expression_number2 bypassing_write_buffer
                 new_value s2 with
         | ComputationProduces s1', ComputationProduces s2' -> ()
         | ComputationImpossible, ComputationImpossible -> ()
         | ComputationUndefined, ComputationUndefined -> ()
         | _, _ -> false_elim ())
    | _ -> ()
  )

#pop-options
#push-options "--z3rlimit 10"

let rec update_expressions_with_gvars_unaddressed_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expressions vs exps
                    /\ global_variables_unaddressed_in_object_values vs new_values)
          (ensures  (match update_expressions exps actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_values s1,
                           update_expressions exps actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_values s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                            states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_with_gvars_unaddressed_maintains_states_match vs pc_relation
        first_exp actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2
        bypassing_write_buffer first_new_value s1 s2;
      (match update_expression first_exp actor writer_pc1 writer_expression_number1
               bypassing_write_buffer first_new_value s1,
             update_expression first_exp actor writer_pc2 writer_expression_number2
               bypassing_write_buffer first_new_value s2 with
       | ComputationProduces s1_next, ComputationProduces s2_next ->
           update_expressions_with_gvars_unaddressed_maintains_states_match vs pc_relation
             remaining_exps actor writer_pc1 writer_pc2 (writer_expression_number1 + 1) (writer_expression_number2 + 1)
             bypassing_write_buffer remaining_new_values s1_next s2_next;
           (match update_expressions exps actor writer_pc1 writer_expression_number1
                    bypassing_write_buffer new_values s1,
                  update_expressions exps actor writer_pc2 writer_expression_number2
                    bypassing_write_buffer new_values s2 with
            | ComputationProduces s1', ComputationProduces s2' -> ()
            | ComputationImpossible, ComputationImpossible -> ()
            | ComputationUndefined, ComputationUndefined -> ()
            | _, _ -> ())
       | ComputationImpossible, ComputationImpossible -> ()
       | ComputationUndefined, ComputationUndefined -> ()
       | _, _ -> ())
  | _, _ -> ()
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Value.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Pointer.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.UnaryOp.fst.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.Util.fst

    vs: Prims.list Armada.Base.var_id_t ->
    pc_relation: Strategies.PCRelation.pc_relation_t ->
    exps: Prims.list Armada.Expression.expression_t ->
    actor: Armada.Base.tid_t ->
    writer_pc1: Armada.Base.pc_t ->
    writer_pc2: Armada.Base.pc_t ->
    writer_expression_number1: Prims.nat ->
    writer_expression_number2: Prims.nat ->
    bypassing_write_buffer: Prims.bool ->
    new_values: Prims.list Armada.Type.object_value_t ->
    s1: Armada.State.t ->
    s2: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.states_match_except_global_variables vs pc_relation s1 s2 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s1) /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s2) /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s1) /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s2) /\
        ThreadStatusRunning? (Mkt?.status (Mkt?.threads s1 actor)) /\
        Strategies.GlobalVars.global_variables_unmentioned_in_expressions vs exps /\
        Strategies.GlobalVars.expressions_lack_pointer_field exps)
      (ensures
        ((match
              Armada.Expression.update_expressions exps
                actor
                writer_pc1
                writer_expression_number1
                bypassing_write_buffer
                new_values
                s1,
              Armada.Expression.update_expressions exps
                actor
                writer_pc2
                writer_expression_number2
                bypassing_write_buffer
                new_values
                s2
            with
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationProduces #_ s1')
              (Armada.Computation.ComputationProduces #_ s2') ->
              Strategies.GlobalVars.states_match_except_global_variables vs pc_relation s1' s2' /\
              Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s1') /\
              Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s2') /\
              Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s1') /\
              Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s2') /\
              ThreadStatusRunning? (Mkt?.status (Mkt?.threads s1' actor))
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationImpossible #_)
              (Armada.Computation.ComputationImpossible #_) ->
              Prims.l_True
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationUndefined #_)
              (Armada.Computation.ComputationUndefined #_) ->
              Prims.l_True
            | _ -> Prims.l_False)
          <:
          Type0))
Prims.list Armada.Base.var_id_t Strategies.PCRelation.pc_relation_t Armada.Expression.expression_t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t FStar.Pervasives.Native.Mktuple2 Armada.Computation.conditional_computation_t Armada.Expression.update_expression Armada.Expression.update_expressions Prims.unit Strategies.GlobalVars.Util.update_expressions_lacking_pointer_field_maintains_states_match Prims.op_Addition Strategies.GlobalVars.Util.update_expression_lacking_pointer_field_maintains_states_match Prims.l_and Strategies.GlobalVars.states_match_except_global_variables Strategies.GlobalVars.global_variables_unaddressed_in_memory Armada.State.__proj__Mkt__item__mem Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.b2t Armada.Thread.uu___is_ThreadStatusRunning Armada.Thread.__proj__Mkt__item__status Armada.State.__proj__Mkt__item__threads Strategies.GlobalVars.global_variables_unmentioned_in_expressions Strategies.GlobalVars.expressions_lack_pointer_field Prims.squash Prims.l_True FStar.Pervasives.Native.tuple2 Prims.l_False Prims.Nil FStar.Pervasives.pattern
let rec update_expressions_lacking_pointer_field_maintains_states_match
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (exps: list expression_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (bypassing_write_buffer: bool)
      (new_values: list object_value_t)
      (s1 s2: Armada.State.t)
    : Lemma
      (requires
        states_match_except_global_variables vs pc_relation s1 s2 /\
        global_variables_unaddressed_in_memory vs s1.mem /\
        global_variables_unaddressed_in_memory vs s2.mem /\ roots_match s1.mem /\ roots_match s2.mem /\
        ThreadStatusRunning? (s1.threads actor).status /\
        global_variables_unmentioned_in_expressions vs exps /\ expressions_lack_pointer_field exps)
      (ensures
        (match
            update_expressions exps
              actor
              writer_pc1
              writer_expression_number1
              bypassing_write_buffer
              new_values
              s1,
            update_expressions exps
              actor
              writer_pc2
              writer_expression_number2
              bypassing_write_buffer
              new_values
              s2
          with
          | ComputationProduces s1', ComputationProduces s2' ->
            states_match_except_global_variables vs pc_relation s1' s2' /\
            global_variables_unaddressed_in_memory vs s1'.mem /\
            global_variables_unaddressed_in_memory vs s2'.mem /\ roots_match s1'.mem /\
            roots_match s2'.mem /\ ThreadStatusRunning? (s1'.threads actor).status
          | ComputationImpossible, ComputationImpossible -> True
          | ComputationUndefined, ComputationUndefined -> True
          | _ -> False)) =
  
match exps, new_values with
| [], [] -> ()
| first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
  update_expression_lacking_pointer_field_maintains_states_match vs pc_relation first_exp actor
    writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2 bypassing_write_buffer
    first_new_value s1 s2;
  (match
      update_expression first_exp
        actor
        writer_pc1
        writer_expression_number1
        bypassing_write_buffer
        first_new_value
        s1,
      update_expression first_exp
        actor
        writer_pc2
        writer_expression_number2
        bypassing_write_buffer
        first_new_value
        s2
    with
    | ComputationProduces s1_next, ComputationProduces s2_next ->
      update_expressions_lacking_pointer_field_maintains_states_match vs pc_relation remaining_exps
        actor writer_pc1 writer_pc2 (writer_expression_number1 + 1) (writer_expression_number2 + 1)
        bypassing_write_buffer remaining_new_values s1_next s2_next;
      (match
          update_expressions exps
            actor
            writer_pc1
            writer_expression_number1
            bypassing_write_buffer
            new_values
            s1,
          update_expressions exps
            actor
            writer_pc2
            writer_expression_number2
            bypassing_write_buffer
            new_values
            s2
        with
        | ComputationProduces s1', ComputationProduces s2' -> ()
        | ComputationImpossible, ComputationImpossible -> ()
        | ComputationUndefined, ComputationUndefined -> ()
        | _, _ -> ())
    | ComputationImpossible, ComputationImpossible -> ()
    | ComputationUndefined, ComputationUndefined -> ()
    | _, _ -> ())
| _, _ -> ()