val successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation
      (sem: semantics_t)
      (actor: sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (steps: list (list sem.step_t))
      (s 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)
val successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation
      (sem: semantics_t)
      (actor: sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (steps: list (list sem.step_t))
      (s 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)
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'
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')
/
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 ->
    actor: Mksemantics_t?.actor_t sem ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    steps: Prims.list (Prims.list (Mksemantics_t?.step_t sem)) ->
    s: Mksemantics_t?.state_t sem ->
    s': Mksemantics_t?.state_t sem
  -> FStar.Pervasives.Lemma
      (requires
        Some? (Strategies.Semantics.steps_computation_generic (Strategies.Atomic.make_atomic_semantics
                  sem)
              actor
              starts_atomic_block
              ends_atomic_block
              steps
              s))
      (ensures
        Strategies.Semantics.steps_computation_generic (Strategies.Atomic.make_atomic_semantics sem)
          actor
          starts_atomic_block
          ends_atomic_block
          steps
          s ==
        Strategies.AtomicToRegular.list_of_list_of_steps_computation sem
          actor
          starts_atomic_block
          ends_atomic_block
          steps
          s)
      (decreases steps)
Strategies.Semantics.semantics_t Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.bool Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.AtomicToRegular.successful_generic_atomic_step_computation_equivalent_to_list_of_list_of_steps_computation FStar.Pervasives.Native.__proj__Some__item__v Strategies.Semantics.steps_computation_generic Prims.unit Prims.b2t FStar.Pervasives.Native.uu___is_Some Strategies.Atomic.make_atomic_semantics Prims.squash Prims.eq2 FStar.Pervasives.Native.option Strategies.AtomicToRegular.list_of_list_of_steps_computation Prims.Nil FStar.Pervasives.pattern
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 ends_atomic_block: bool)
      (steps: list (list sem.step_t))
      (s 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'