val step_lifter_works
      (lsem: semantics_t)
      (hsem: semantics_t{hsem.actor_t == lsem.actor_t})
      (lprog: program_t lsem)
      (hprog: program_t hsem)
      (aux_t: Type)
      (lh_relation: (aux_t -> lsem.state_t -> hsem.state_t -> GTot ubool))
      (progress_t: Type)
      (progress_wfr: wfr_t progress_t)
      (progress_measure: (hsem.state_t -> lsem.step_t -> lsem.actor_t -> GTot progress_t))
      (actor: lsem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: lsem.step_t)
      (ls: lsem.state_t)
      (hs: hsem.state_t)
      (lifter: step_lifter_t hsem.step_t aux_t)
    : GTot ubool
val step_lifter_works
      (lsem: semantics_t)
      (hsem: semantics_t{hsem.actor_t == lsem.actor_t})
      (lprog: program_t lsem)
      (hprog: program_t hsem)
      (aux_t: Type)
      (lh_relation: (aux_t -> lsem.state_t -> hsem.state_t -> GTot ubool))
      (progress_t: Type)
      (progress_wfr: wfr_t progress_t)
      (progress_measure: (hsem.state_t -> lsem.step_t -> lsem.actor_t -> GTot progress_t))
      (actor: lsem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: lsem.step_t)
      (ls: lsem.state_t)
      (hs: hsem.state_t)
      (lifter: step_lifter_t hsem.step_t aux_t)
    : GTot ubool
let step_lifter_works
  (lsem: semantics_t)
  (hsem: semantics_t{hsem.actor_t == lsem.actor_t})
  (lprog: program_t lsem)
  (hprog: program_t hsem)
  (aux_t: Type)
  (lh_relation: aux_t -> lsem.state_t -> hsem.state_t -> GTot ubool)
  (progress_t: Type)
  (progress_wfr: wfr_t progress_t)
  (progress_measure: hsem.state_t -> lsem.step_t -> lsem.actor_t -> GTot progress_t)
  (actor: lsem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lstep: lsem.step_t)
  (ls: lsem.state_t)
  (hs: hsem.state_t)
  (lifter: step_lifter_t hsem.step_t aux_t)
  : GTot ubool =
  match lifter with
  | StepLifterSkip aux' ->
      (match step_computation_generic lsem actor starts_atomic_block ends_atomic_block lstep ls with
       | Some ls' ->
             lh_relation aux' ls' hs
           /\ (starts_atomic_block = ends_atomic_block)
       | None -> False)
  | StepLifterIntroduce hstep aux' ->
      (* Introduced steps must have ends_atomic_block the same as starts_atomic_block *)
      (match step_computation_generic hsem actor starts_atomic_block starts_atomic_block hstep hs with
       | Some hs' ->
             lh_relation aux' ls hs'
           /\ program_contains_action_of_step_generic hsem hprog hstep
           /\ progress_wfr.relation (progress_measure hs' lstep actor) (progress_measure hs lstep actor)
       | None -> False)
  | StepLifterLift hstep aux' ->
      (match step_computation_generic lsem actor starts_atomic_block ends_atomic_block lstep ls,
             step_computation_generic hsem actor starts_atomic_block ends_atomic_block hstep hs with
       | Some ls', Some hs' ->
             program_contains_action_of_step_generic hsem hprog hstep
           /\ lh_relation aux' ls' hs'
       | _, _ -> False)
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

noeq type step_lifter_t (step_t: Type) (aux_t: Type) =
  | StepLifterSkip: (aux': aux_t) -> step_lifter_t step_t aux_t
  | StepLifterIntroduce: (hstep: step_t) -> (aux': aux_t) -> step_lifter_t step_t aux_t
  | StepLifterLift: (hstep: step_t) -> (aux': aux_t) -> step_lifter_t step_t aux_t
/
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
Strategies.Lift.Generic.fsti

    lsem: Strategies.Semantics.semantics_t ->
    hsem:
      Strategies.Semantics.semantics_t{Mksemantics_t?.actor_t hsem == Mksemantics_t?.actor_t lsem} ->
    lprog: Strategies.Semantics.program_t lsem ->
    hprog: Strategies.Semantics.program_t hsem ->
    aux_t: Type ->
    lh_relation:
      (_: aux_t -> _: Mksemantics_t?.state_t lsem -> _: Mksemantics_t?.state_t hsem
          -> Prims.GTot Spec.Ubool.ubool) ->
    progress_t: Type ->
    progress_wfr: FStar.WellFoundedRelation.wfr_t progress_t ->
    progress_measure:
      (
            _: Mksemantics_t?.state_t hsem ->
            _: Mksemantics_t?.step_t lsem ->
            _: Mksemantics_t?.actor_t lsem
          -> Prims.GTot progress_t) ->
    actor: Mksemantics_t?.actor_t lsem ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    lstep: Mksemantics_t?.step_t lsem ->
    ls: Mksemantics_t?.state_t lsem ->
    hs: Mksemantics_t?.state_t hsem ->
    lifter: Strategies.Lift.Generic.step_lifter_t (Mksemantics_t?.step_t hsem) aux_t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.semantics_t Prims.eq2 Prims.eqtype Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Semantics.program_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Spec.Ubool.ubool FStar.WellFoundedRelation.wfr_t Strategies.Semantics.__proj__Mksemantics_t__item__step_t Prims.bool Strategies.Lift.Generic.step_lifter_t Strategies.Semantics.step_computation_generic Prims.l_and Prims.b2t Prims.op_Equality Prims.l_False Strategies.Semantics.program_contains_action_of_step_generic FStar.WellFoundedRelation.__proj__Mkwfr_t__item__relation FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option
let step_lifter_works
      (lsem: semantics_t)
      (hsem: semantics_t{hsem.actor_t == lsem.actor_t})
      (lprog: program_t lsem)
      (hprog: program_t hsem)
      (aux_t: Type)
      (lh_relation: (aux_t -> lsem.state_t -> hsem.state_t -> GTot ubool))
      (progress_t: Type)
      (progress_wfr: wfr_t progress_t)
      (progress_measure: (hsem.state_t -> lsem.step_t -> lsem.actor_t -> GTot progress_t))
      (actor: lsem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: lsem.step_t)
      (ls: lsem.state_t)
      (hs: hsem.state_t)
      (lifter: step_lifter_t hsem.step_t aux_t)
    : GTot ubool =
  
match lifter with
| StepLifterSkip aux' ->
  (match step_computation_generic lsem actor starts_atomic_block ends_atomic_block lstep ls with
    | Some ls' -> lh_relation aux' ls' hs /\ (starts_atomic_block = ends_atomic_block)
    | None -> False)
| StepLifterIntroduce hstep aux' ->
  (match step_computation_generic hsem actor starts_atomic_block starts_atomic_block hstep hs with
    | Some hs' ->
      lh_relation aux' ls hs' /\ program_contains_action_of_step_generic hsem hprog hstep /\
      progress_wfr.relation (progress_measure hs' lstep actor) (progress_measure hs lstep actor)
    | None -> False)
| StepLifterLift hstep aux' ->
  (match
      step_computation_generic lsem actor starts_atomic_block ends_atomic_block lstep ls,
      step_computation_generic hsem actor starts_atomic_block ends_atomic_block hstep hs
    with
    | Some ls', Some hs' ->
      program_contains_action_of_step_generic hsem hprog hstep /\ lh_relation aux' ls' hs'
    | _, _ -> False)