val flatten_transition_preserves_next_transition
      (sem: semantics_t)
      (ltr: transition_t (make_atomic_semantics sem))
      (htr: transition_t sem)
      (s s': sem.state_t)
    : Lemma
      (requires
        htr.steps == flatten ltr.steps /\
        next_transition_generic (make_atomic_semantics sem) ltr s s' /\ htr.actor == ltr.actor)
      (ensures next_transition_generic sem htr s s')
val flatten_transition_preserves_next_transition
      (sem: semantics_t)
      (ltr: transition_t (make_atomic_semantics sem))
      (htr: transition_t sem)
      (s s': sem.state_t)
    : Lemma
      (requires
        htr.steps == flatten ltr.steps /\
        next_transition_generic (make_atomic_semantics sem) ltr s s' /\ htr.actor == ltr.actor)
      (ensures next_transition_generic sem htr s s')
let flatten_transition_preserves_next_transition
  (sem: semantics_t)
  (ltr: transition_t (make_atomic_semantics sem))
  (htr: transition_t sem)
  (s: sem.state_t)
  (s': sem.state_t)
  : Lemma
  (requires   htr.steps == flatten ltr.steps
            /\ next_transition_generic (make_atomic_semantics sem) ltr s s'
            /\ htr.actor == ltr.actor)
  (ensures  next_transition_generic sem htr s s') =
  let atomic_sem = make_atomic_semantics sem in
  let unflattened_steps = ltr.steps in
  successful_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation sem ltr s s';
  atomic_steps_computation_implies_nonempty_steps sem ltr.actor true true unflattened_steps s;
  flatten_steps_preserves_eval_result sem ltr.actor true true htr.steps unflattened_steps s
module Strategies.AtomicToRegular

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

let steps_then_steps_computation
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps1: list sem.step_t)
  (steps2: list sem.step_t)
  (s: sem.state_t)
  : GTot (option sem.state_t) =
  match steps_computation_generic sem actor starts_atomic_block false steps1 s with
  | None -> None
  | Some s' -> steps_computation_generic sem actor false ends_atomic_block steps2 s'

let rec steps_then_steps_computation_equivalent_to_append_compute
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps1: list sem.step_t)
  (steps2: list sem.step_t)
  (s: sem.state_t)
  : Lemma
  (requires Cons? steps1 /\ Cons? steps2)
  (ensures  steps_then_steps_computation sem actor starts_atomic_block ends_atomic_block steps1 steps2 s ==
            steps_computation_generic sem actor starts_atomic_block ends_atomic_block (append steps1 steps2) s)
  (decreases steps1) =
  match steps1 with
  | [last_step] -> ()
  | first_step :: remaining_steps ->
      (match step_computation_generic sem actor starts_atomic_block false first_step s with
       | None -> ()
       | Some s' -> steps_then_steps_computation_equivalent_to_append_compute sem actor
                     false ends_atomic_block remaining_steps steps2 s')

let rec list_of_list_of_steps_computation
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps: list (list sem.step_t))
  (s: sem.state_t)
  : GTot (option sem.state_t)
      (decreases steps) =
  match steps with
  | [] -> None
  | [last_step] -> steps_computation_generic sem actor starts_atomic_block ends_atomic_block last_step s
  | first_step :: remaining_steps ->
      (match steps_computation_generic sem actor starts_atomic_block false first_step s with
       | None -> None
       | Some s' -> list_of_list_of_steps_computation sem actor false ends_atomic_block remaining_steps s')

let rec successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps: list (list sem.step_t))
  (s: sem.state_t)
  (s': sem.state_t)
  : Lemma (requires Some? (steps_computation_generic (make_atomic_semantics sem) actor starts_atomic_block
                             ends_atomic_block steps s))
          (ensures  steps_computation_generic (make_atomic_semantics sem) actor starts_atomic_block
                      ends_atomic_block steps s ==
                        list_of_list_of_steps_computation sem actor starts_atomic_block ends_atomic_block steps s)
          (decreases steps) =
  match steps with
  | [] -> ()
  | [last_atomic_step] -> ()
  | first_step :: remaining_steps ->
      let s_mid = Some?.v (steps_computation_generic sem actor starts_atomic_block false first_step s) in
      successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation sem actor false
        ends_atomic_block remaining_steps s_mid s'

let successful_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation
  (sem: semantics_t)
  (transition: transition_t (make_atomic_semantics sem))
  (s: sem.state_t)
  (s': sem.state_t)
  : Lemma (requires next_transition_generic (make_atomic_semantics sem) transition s s')
          (ensures  steps_computation_generic (make_atomic_semantics sem) transition.actor true true
                      transition.steps s ==
                      list_of_list_of_steps_computation sem transition.actor true true transition.steps s)
          (decreases transition.steps) =
  successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation sem transition.actor
    true true transition.steps s s'

let rec flatten_steps_preserves_eval_result
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (flattened_steps: list sem.step_t)
  (unflattened_steps: list (list sem.step_t))
  (s: sem.state_t)
  : Lemma
  (requires   flattened_steps == flatten unflattened_steps
            /\ (forall steps. contains_ubool steps unflattened_steps ==> Cons? steps)
            /\ Some? (list_of_list_of_steps_computation sem actor starts_atomic_block ends_atomic_block
                       unflattened_steps s))
  (ensures  (steps_computation_generic sem actor starts_atomic_block ends_atomic_block flattened_steps s) ==
            (list_of_list_of_steps_computation sem actor starts_atomic_block ends_atomic_block unflattened_steps s))
  (decreases unflattened_steps) =
  match unflattened_steps with
  | [] -> ()
  | [last_atomic_step] -> append_nil_is_identity last_atomic_step
  | first_atomic_step :: remaining_unflattened_steps ->
     let remaining_steps = flatten remaining_unflattened_steps in
     assert (contains_ubool first_atomic_step unflattened_steps);
     steps_then_steps_computation_equivalent_to_append_compute sem actor starts_atomic_block ends_atomic_block
       first_atomic_step remaining_steps s;
     (match steps_computation_generic sem actor starts_atomic_block false first_atomic_step s with
      | None -> ()
      | Some s' -> flatten_steps_preserves_eval_result sem actor false ends_atomic_block remaining_steps
                    remaining_unflattened_steps s')

let rec atomic_steps_computation_implies_nonempty_steps
  (sem: semantics_t)
  (actor: sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (atomic_steps: list (list sem.step_t))
  (s: sem.state_t)
  : Lemma (requires Some? (list_of_list_of_steps_computation sem actor starts_atomic_block ends_atomic_block
                             atomic_steps s))
          (ensures  forall atomic_step. contains_ubool atomic_step atomic_steps ==> Cons? atomic_step)
          (decreases atomic_steps) =
  match atomic_steps with
  | [last_atomic_step] -> ()
  | first_atomic_step :: remaining_atomic_steps ->
      let s' = Some?.v (steps_computation_generic sem actor starts_atomic_block false first_atomic_step s) in
      atomic_steps_computation_implies_nonempty_steps sem actor false ends_atomic_block remaining_atomic_steps s'
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.AtomicToRegular.fst

    sem: Strategies.Semantics.semantics_t ->
    ltr: Strategies.Semantics.transition_t (Strategies.Atomic.make_atomic_semantics sem) ->
    htr: Strategies.Semantics.transition_t sem ->
    s: Mksemantics_t?.state_t sem ->
    s': Mksemantics_t?.state_t sem
  -> FStar.Pervasives.Lemma
      (requires
        Mktransition_t?.steps htr == FStar.List.Tot.Base.flatten (Mktransition_t?.steps ltr) /\
        Strategies.Semantics.next_transition_generic (Strategies.Atomic.make_atomic_semantics sem)
          ltr
          s
          s' /\ Mktransition_t?.actor htr == Mktransition_t?.actor ltr)
      (ensures Strategies.Semantics.next_transition_generic sem htr s s')
Strategies.Semantics.semantics_t Strategies.Semantics.transition_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.AtomicToRegular.flatten_steps_preserves_eval_result Strategies.Semantics.__proj__Mktransition_t__item__actor Strategies.Semantics.__proj__Mktransition_t__item__steps Prims.unit Strategies.AtomicToRegular.atomic_steps_computation_implies_nonempty_steps Strategies.AtomicToRegular.successful_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Prims.l_and Prims.eq2 FStar.List.Tot.Base.flatten Strategies.Semantics.next_transition_generic Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.squash Prims.Nil FStar.Pervasives.pattern
let flatten_transition_preserves_next_transition
      (sem: semantics_t)
      (ltr: transition_t (make_atomic_semantics sem))
      (htr: transition_t sem)
      (s s': sem.state_t)
    : Lemma
      (requires
        htr.steps == flatten ltr.steps /\
        next_transition_generic (make_atomic_semantics sem) ltr s s' /\ htr.actor == ltr.actor)
      (ensures next_transition_generic sem htr s s') =
  
let atomic_sem = make_atomic_semantics sem in
let unflattened_steps = ltr.steps in
successful_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation sem ltr s s';
atomic_steps_computation_implies_nonempty_steps sem ltr.actor true true unflattened_steps s;
flatten_steps_preserves_eval_result sem ltr.actor true true htr.steps unflattened_steps s