val refinement_choice_works
      (lr: liftability_relation_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (steps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs: lr.hsem.state_t)
      (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t)
    : GTot ubool
val refinement_choice_works
      (lr: liftability_relation_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (steps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs: lr.hsem.state_t)
      (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t)
    : GTot ubool
let refinement_choice_works
  (lr: liftability_relation_t)
  (ls: lr.lsem.state_t)
  (actor: lr.lsem.actor_t)
  (starts_atomic_block: bool)
  (steps: list lr.lsem.step_t)
  (ls': lr.lsem.state_t)
  (hs: lr.hsem.state_t)
  (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t)
  : GTot ubool =
  match choice with
  | RefinementChoiceSkip aux' ->
         starts_atomic_block
      /\ lr.inv ls'
      /\ lr.lh_relation aux' ls' hs
  | RefinementChoiceIntroduce hsteps hs' aux' ->
         starts_atomic_block
      /\ for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps
      /\ Some hs' == steps_computation_generic lr.hsem actor starts_atomic_block true
                      hsteps hs
      /\ lr.lh_relation aux' ls hs'
      /\ (match steps with
         | [] -> False
         | lstep :: _ ->
             lr.progress_wfr.relation (lr.progress_measure hs' lstep actor) (lr.progress_measure hs lstep actor))
  | RefinementChoiceLift hsteps hs' aux' ->
        for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps
      /\ (Some hs') == steps_computation_generic lr.hsem actor starts_atomic_block true
                        hsteps hs
      /\ lr.inv ls'
      /\ lr.lh_relation aux' ls' hs'
module Strategies.Lift.Generic

open FStar.WellFoundedRelation
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Invariant
open Strategies.Semantics
open Util.List
open Util.Logic

noeq type refinement_choice_t (step_t: Type) (state_t: Type) (aux_t: Type) =
  | RefinementChoiceSkip: (aux': aux_t) -> refinement_choice_t step_t state_t aux_t
  | RefinementChoiceIntroduce: (steps: list step_t) -> (state: state_t) -> (aux': aux_t) ->
                               refinement_choice_t step_t state_t aux_t
  | RefinementChoiceLift: (steps: list step_t) -> (state: state_t) -> (aux': aux_t) ->
                          refinement_choice_t step_t state_t aux_t
/
Util.Logic.fst.checked Util.List.fst.checked Strategies.Semantics.fst.checked Strategies.Invariant.fsti.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.WellFoundedRelation.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked
Strategies.Lift.Generic.fst

    lr: Strategies.Lift.Generic.liftability_relation_t ->
    ls: Mksemantics_t?.state_t (Mkliftability_relation_t?.lsem lr) ->
    actor: Mksemantics_t?.actor_t (Mkliftability_relation_t?.lsem lr) ->
    starts_atomic_block: Prims.bool ->
    steps: Prims.list (Mksemantics_t?.step_t (Mkliftability_relation_t?.lsem lr)) ->
    ls': Mksemantics_t?.state_t (Mkliftability_relation_t?.lsem lr) ->
    hs: Mksemantics_t?.state_t (Mkliftability_relation_t?.hsem lr) ->
    choice:
      Strategies.Lift.Generic.refinement_choice_t (Mksemantics_t?.step_t (Mkliftability_relation_t?.hsem
                lr))
        (Mksemantics_t?.state_t (Mkliftability_relation_t?.hsem lr))
        (Mkliftability_relation_t?.aux_t lr)
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Lift.Generic.liftability_relation_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__lsem Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.bool Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__hsem Strategies.Lift.Generic.refinement_choice_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__aux_t Prims.l_and Prims.b2t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__inv Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__lh_relation Util.List.for_all_ubool Strategies.Semantics.program_contains_action_of_step_generic Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__hprog Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.Some Strategies.Semantics.steps_computation_generic Prims.l_False FStar.WellFoundedRelation.__proj__Mkwfr_t__item__relation Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__progress_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__progress_wfr Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__progress_measure Prims.logical Spec.Ubool.ubool
let refinement_choice_works
      (lr: liftability_relation_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (steps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs: lr.hsem.state_t)
      (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t)
    : GTot ubool =
  
match choice with
| RefinementChoiceSkip aux' -> starts_atomic_block /\ lr.inv ls' /\ lr.lh_relation aux' ls' hs
| RefinementChoiceIntroduce hsteps hs' aux' ->
  starts_atomic_block /\
  for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps /\
  Some hs' == steps_computation_generic lr.hsem actor starts_atomic_block true hsteps hs /\
  lr.lh_relation aux' ls hs' /\
  (match steps with
    | [] -> False
    | lstep :: _ ->
      lr.progress_wfr.relation (lr.progress_measure hs' lstep actor)
        (lr.progress_measure hs lstep actor))
| RefinementChoiceLift hsteps hs' aux' ->
  for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps /\
  (Some hs') == steps_computation_generic lr.hsem actor starts_atomic_block true hsteps hs /\
  lr.inv ls' /\ lr.lh_relation aux' ls' hs'