The Machine Strategy (§ 5.3)

Having defined the OGS game and axiomatized the language machine, we are now ready to construct the machine strategy.

We consider a language abstractly captured as a machine.

  Context `{CC : context T C} {CL : context_laws T C}.
  Context {val} {VM : subst_monoid val} {VML : subst_monoid_laws val}.
  Context {conf} {CM : subst_module val conf} {CML : subst_module_laws val conf}.
  Context {obs : obs_struct T C} {M : machine val conf obs}.

We start off by defining active and passive OGS assignments (Def 5.16). This datastructure will hold the memory part of a strategy state, remembering the values which we have hidden from Opponent and given as fresh variables.

  Inductive ogs_env (Δ : C) : polarity -> ogs_ctx -> Type :=
  | ENilA : ogs_env Δ Act ∅ₓ
  | ENilP : ogs_env Δ Pas ∅ₓ
  | EConA {Φ Γ} : ogs_env Δ Pas Φ -> ogs_env Δ Act (Φ ▶ₓ Γ)
  | EConP {Φ Γ} : ogs_env Δ Act Φ -> Γ =[val]> (Δ +▶ ↓⁺Φ) -> ogs_env Δ Pas (Φ ▶ₓ Γ)
  .

  Notation "'ε⁺'" := (ENilA).
  Notation "'ε⁻'" := (ENilP).
  Notation "u ;⁺" := (EConA u).
  Notation "u ;⁻ e" := (EConP u e).

Next we define the collapsing function on OGS assignments (Def 5.18).

  Equations collapse {Δ p Φ} : ogs_env Δ p Φ -> ↓[p^]Φ =[val]> (Δ +▶ ↓[p]Φ) :=
    collapse ε⁺       := ! ;
    collapse ε⁻       := ! ;
    collapse (u ;⁺)   := collapse u ⊛ᵣ r_cat3_1 ;
    collapse (u ;⁻ e) := [ collapse u , e ] .
  Notation "ₐ↓ γ" := (collapse γ).

We readily define the zipping function (Def 6.10).

  #[derive(eliminator=no)]
  Equations bicollapse {Δ} Φ : ogs_env Δ Act Φ -> ogs_env Δ Pas Φ -> forall p, ↓[p]Φ =[val]> Δ :=
    bicollapse ∅ₓ       (ε⁺)     (ε⁻)     Act   := ! ;
    bicollapse ∅ₓ       (ε⁺)     (ε⁻)     Pas   := ! ;
    bicollapse (Φ ▶ₓ _) (u ;⁺)   (v ;⁻ γ) Act :=
          [ bicollapse Φ v u Pas , γ ⊛ [ a_id , bicollapse Φ v u Act ] ] ;
    bicollapse (Φ ▶ₓ _) (v ;⁺)   (u ;⁻ e) Pas := bicollapse Φ u v Act .
  #[global] Arguments bicollapse {Δ Φ} u v {p}.

And the fixpoint property linking collapsing and zipping (Prop 6.13).

  Lemma collapse_fix_aux {Δ Φ} (u : ogs_env Δ Act Φ) (v : ogs_env Δ Pas Φ)
    :  ₐ↓u ⊛ [ a_id , bicollapse u v ] ≡ₐ bicollapse u v
     /\ ₐ↓v ⊛ [ a_id , bicollapse u v ] ≡ₐ bicollapse u v .
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
    induction Φ; dependent destruction u; dependent destruction v.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
ₐ↓ ε⁺ ⊛ [a_id, bicollapse ε⁺ ε⁻] ≡ₐ bicollapse ε⁺ ε⁻ /\
ₐ↓ ε⁻ ⊛ [a_id, bicollapse ε⁺ ε⁻] ≡ₐ bicollapse ε⁺ ε⁻
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
ₐ↓ (u;⁺) ⊛ [a_id, bicollapse (u;⁺) (v;⁻ a)]
≡ₐ bicollapse (u;⁺) (v;⁻ a) /\
ₐ↓ (v;⁻ a) ⊛ [a_id, bicollapse (u;⁺) (v;⁻ a)]
≡ₐ bicollapse (u;⁺) (v;⁻ a)
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
ₐ↓ ε⁺ ⊛ [a_id, bicollapse ε⁺ ε⁻] ≡ₐ bicollapse ε⁺ ε⁻ /\
ₐ↓ ε⁻ ⊛ [a_id, bicollapse ε⁺ ε⁻] ≡ₐ bicollapse ε⁺ ε⁻ split; intros ? i; now destruct (c_view_emp i).
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
ₐ↓ (u;⁺) ⊛ [a_id, bicollapse (u;⁺) (v;⁻ a)]
≡ₐ bicollapse (u;⁺) (v;⁻ a) /\
ₐ↓ (v;⁻ a) ⊛ [a_id, bicollapse (u;⁺) (v;⁻ a)]
≡ₐ bicollapse (u;⁺) (v;⁻ a) split; cbn; simp collapse; simp bicollapse.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
(ₐ↓ u ⊛ᵣ r_cat3_1)
⊛ [a_id, [bicollapse v u, a ⊛ [a_id, bicollapse v u]]]
≡ₐ bicollapse v u
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
[ₐ↓ v, a] ⊛ [a_id, bicollapse v u]
≡ₐ [bicollapse v u, a ⊛ [a_id, bicollapse v u]]
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
(ₐ↓ u ⊛ᵣ r_cat3_1)
⊛ [a_id, [bicollapse v u, a ⊛ [a_id, bicollapse v u]]]
≡ₐ bicollapse v u intros ? i; cbn; rewrite <- v_sub_sub, a_ren_r_simpl, r_cat3_1_simpl.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
a0: T
i: ↓⁺ Φ ∋ a0
ₐ↓ u a0 i ᵥ⊛ [a_id, bicollapse v u] =
bicollapse v u a0 i
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
a0: T
i: ↓⁺ Φ ∋ a0
subst_monoid_laws val
        now apply IHΦ.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
a0: T
i: ↓⁺ Φ ∋ a0
subst_monoid_laws val
        exact _. (* wtf typeclass?? *)
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
[ₐ↓ v, a] ⊛ [a_id, bicollapse v u]
≡ₐ [bicollapse v u, a ⊛ [a_id, bicollapse v u]] intros ? i; cbn; destruct (c_view_cat i); eauto.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ctx C
x: C
u: ogs_env Δ Pas Φ
v: ogs_env Δ Act Φ
a: x =[ val ]> (Δ +▶ ↓⁺ Φ)
IHΦ: forall (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ),
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v /\
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
a0: T
i: ↓⁻ Φ ∋ a0
ₐ↓ v a0 i ᵥ⊛ [a_id, bicollapse v u] =
bicollapse v u a0 i
        now apply IHΦ.
  Qed.

  Lemma collapse_fix_act {Δ Φ} (u : ogs_env Δ Act Φ) (v : ogs_env Δ Pas Φ)
    : ₐ↓u ⊛ [ a_id , bicollapse u v ] ≡ₐ bicollapse u v .
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ u ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v now apply collapse_fix_aux. Qed.

  Lemma collapse_fix_pas {Δ Φ} (u : ogs_env Δ Act Φ) (v : ogs_env Δ Pas Φ)
    : ₐ↓v ⊛ [ a_id , bicollapse u v ] ≡ₐ bicollapse u v .
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
ₐ↓ v ⊛ [a_id, bicollapse u v] ≡ₐ bicollapse u v now apply collapse_fix_aux. Qed.

Here we provide an alternative definition to the collapsing functions, using a more precisely typed lookup function. This is more practical to use when reasoning about the height of a variable, in the eventual guardedness proof.

First we compute actual useful subset of the context used by a particular variable.

  Equations ctx_dom Φ p {x} : ↓[p^]Φ ∋ x -> C :=
    ctx_dom ∅ₓ       Act i with c_view_emp i := { | ! } ;
    ctx_dom ∅ₓ       Pas i with c_view_emp i := { | ! } ;
    ctx_dom (Φ ▶ₓ Γ) Act i := ctx_dom Φ Pas i ;
    ctx_dom (Φ ▶ₓ Γ) Pas i with c_view_cat i := {
      | Vcat_l j := ctx_dom Φ Act j ;
      | Vcat_r j := ↓[Act]Φ } .
  #[global] Arguments ctx_dom {Φ p x} i.

Next we provide a renaming from this precise domain to the actual current allowed context.

  Equations r_ctx_dom Φ p {x} (i : ↓[p^]Φ ∋ x) : ctx_dom i ⊆ ↓[p]Φ :=
    r_ctx_dom ∅ₓ       Act i with c_view_emp i := { | ! } ;
    r_ctx_dom ∅ₓ       Pas i with c_view_emp i := { | ! } ;
    r_ctx_dom (Φ ▶ₓ Γ) Act i := r_ctx_dom Φ Pas i ᵣ⊛ r_cat_l ;
    r_ctx_dom (Φ ▶ₓ Γ) Pas i with c_view_cat i := {
      | Vcat_l j := r_ctx_dom Φ Act j ;
      | Vcat_r j := r_id } .
  #[global] Arguments r_ctx_dom {Φ p x} i.

We can write this more precise lookup function, returning a value in just the necessary context.

  Equations lookup {Δ p Φ} (γ : ogs_env Δ p Φ) [x] (i : ↓[p^]Φ ∋ x)
            : val (Δ +▶ ctx_dom i) x :=
    lookup ε⁺       i with c_view_emp i := { | ! } ;
    lookup ε⁻       i with c_view_emp i := { | ! } ;
    lookup (γ ;⁺)   i := lookup γ i ;
    lookup (γ ;⁻ e) i with c_view_cat i := {
      | Vcat_l j := lookup γ j ;
      | Vcat_r j := e _ j } .

We relate the precise lookup with the previously defined collapse.

  Lemma lookup_collapse {Δ p Φ} (γ : ogs_env Δ p Φ) :
    collapse γ ≡ₐ (fun x i => lookup γ i ᵥ⊛ᵣ [ r_cat_l , r_ctx_dom i ᵣ⊛ r_cat_r ]).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
p: polarity
Φ: ogs_ctx
γ: ogs_env Δ p Φ
ₐ↓ γ
≡ₐ (fun (x : T) (i : ↓[ p ^] Φ ∋ x) =>
    lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r])
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
p: polarity
Φ: ogs_ctx
γ: ogs_env Δ p Φ
ₐ↓ γ
≡ₐ (fun (x : T) (i : ↓[ p ^] Φ ∋ x) =>
    lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r])
    intros ? i; funelim (lookup γ i).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
ₐ↓ (γ;⁺) x i =
lookup (γ;⁺) i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: (fix join_pol
   (p : polarity) (o : ogs_ctx) {struct o} : C :=
   match p with
   | Act =>
       fun o0 : ogs_ctx =>
       match o0 with
       | ∅ₓ => ∅
       | c ▶ₓ c0 => join_pol Pas c +▶ c0
       end
   | Pas =>
       fun o0 : ogs_ctx =>
       match o0 with
       | ∅ₓ => ∅
       | c ▶ₓ _ => join_pol Act c
       end
   end o) Pas Φ1 ∋ x
H: ₐ↓ γ x j =
lookup γ j ᵥ⊛ᵣ [r_cat_l, r_ctx_dom j ᵣ⊛ r_cat_r]
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_l j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_l j) refine) x) Heq
  (lookup γ j) = lookup (γ;⁻ e) (r_cat_l j)
ₐ↓ (γ;⁻ e) x (r_cat_l j) =
lookup (γ;⁻ e) (r_cat_l j)
ᵥ⊛ᵣ [r_cat_l, r_ctx_dom (r_cat_l j) ᵣ⊛ r_cat_r]
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: Γ0 ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_r j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_r j) refine) x) Heq 
  (e x j) = lookup (γ;⁻ e) (r_cat_r j)
ₐ↓ (γ;⁻ e) x (r_cat_r j) =
lookup (γ;⁻ e) (r_cat_r j)
ᵥ⊛ᵣ [r_cat_l, r_ctx_dom (r_cat_r j) ᵣ⊛ r_cat_r]
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
ₐ↓ (γ;⁺) x i =
lookup (γ;⁺) i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r] cbn; rewrite H.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
ᵥ⊛ r_emb r_cat3_1 =
lookup γ i
ᵥ⊛ r_emb
     [r_cat_l, (r_ctx_dom i ᵣ⊛ r_cat_l) ᵣ⊛ r_cat_r]
      unfold v_ren; rewrite <- v_sub_sub.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
lookup γ i
ᵥ⊛ r_emb [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
   ⊛ r_emb r_cat3_1 =
lookup γ i
ᵥ⊛ r_emb
     [r_cat_l, (r_ctx_dom i ᵣ⊛ r_cat_l) ᵣ⊛ r_cat_r]
      apply v_sub_proper; eauto.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
r_emb [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
⊛ r_emb r_cat3_1
≡ₐ r_emb
     [r_cat_l, (r_ctx_dom i ᵣ⊛ r_cat_l) ᵣ⊛ r_cat_r]
      intros ? j; cbn; rewrite v_sub_var; cbn; f_equal.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
a: T
j: Δ +▶ ctx_dom i ∋ a
r_cat3_1 a
  match c_view_cat j with
  | Vcat_l i => r_cat_l i
  | Vcat_r j => r_cat_r (r_ctx_dom i a j)
  end =
match c_view_cat j with
| Vcat_l i => r_cat_l i
| Vcat_r j => r_cat_r (r_cat_l (r_ctx_dom i a j))
end
      unfold r_cat3_1; destruct (c_view_cat j); cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
a: T
i0: Δ ∋ a
match c_view_cat (r_cat_l i0) with
| Vcat_l i => r_cat_l i
| Vcat_r j => r_cat_r (r_cat_l j)
end = r_cat_l i0
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
a: T
j: ctx_dom i ∋ a
match c_view_cat (r_cat_r (r_ctx_dom i a j)) with
| Vcat_l i => r_cat_l i
| Vcat_r j => r_cat_r (r_cat_l j)
end = r_cat_r (r_cat_l (r_ctx_dom i a j))
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
a: T
i0: Δ ∋ a
match c_view_cat (r_cat_l i0) with
| Vcat_l i => r_cat_l i
| Vcat_r j => r_cat_r (r_cat_l j)
end = r_cat_l i0 now rewrite c_view_cat_simpl_l.
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ0: ogs_ctx
Γ: C
γ: ogs_env Δ Pas Φ0
x: T
i: ↓[ Act ^] (Φ0 ▶ₓ Γ) ∋ x
H: ₐ↓ γ x i =
lookup γ i ᵥ⊛ᵣ [r_cat_l, r_ctx_dom i ᵣ⊛ r_cat_r]
a: T
j: ctx_dom i ∋ a
match c_view_cat (r_cat_r (r_ctx_dom i a j)) with
| Vcat_l i => r_cat_l i
| Vcat_r j => r_cat_r (r_cat_l j)
end = r_cat_r (r_cat_l (r_ctx_dom i a j)) now rewrite c_view_cat_simpl_r.
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: (fix join_pol
   (p : polarity) (o : ogs_ctx) {struct o} : C :=
   match p with
   | Act =>
       fun o0 : ogs_ctx =>
       match o0 with
       | ∅ₓ => ∅
       | c ▶ₓ c0 => join_pol Pas c +▶ c0
       end
   | Pas =>
       fun o0 : ogs_ctx =>
       match o0 with
       | ∅ₓ => ∅
       | c ▶ₓ _ => join_pol Act c
       end
   end o) Pas Φ1 ∋ x
H: ₐ↓ γ x j =
lookup γ j ᵥ⊛ᵣ [r_cat_l, r_ctx_dom j ᵣ⊛ r_cat_r]
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_l j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_l j) refine) x) Heq
  (lookup γ j) = lookup (γ;⁻ e) (r_cat_l j)
ₐ↓ (γ;⁻ e) x (r_cat_l j) =
lookup (γ;⁻ e) (r_cat_l j)
ᵥ⊛ᵣ [r_cat_l, r_ctx_dom (r_cat_l j) ᵣ⊛ r_cat_r] cbn; rewrite 2 c_view_cat_simpl_l; exact H.
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: Γ0 ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_r j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_r j) refine) x) Heq 
  (e x j) = lookup (γ;⁻ e) (r_cat_r j)
ₐ↓ (γ;⁻ e) x (r_cat_r j) =
lookup (γ;⁻ e) (r_cat_r j)
ᵥ⊛ᵣ [r_cat_l, r_ctx_dom (r_cat_r j) ᵣ⊛ r_cat_r] cbn; rewrite 2 c_view_cat_simpl_r.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: Γ0 ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_r j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_r j) refine) x) Heq 
  (e x j) = lookup (γ;⁻ e) (r_cat_r j)
e x j =
lookup_clause_4 (@lookup) Δ Φ1 Γ0 γ e x 
  (r_cat_r j) (Vcat_r j)
ᵥ⊛ r_emb
     [r_cat_l,
     r_ctx_dom_clause_4 (@r_ctx_dom) Φ1 Γ0 x
       (r_cat_r j) (Vcat_r j) ᵣ⊛ r_cat_r]
      cbn; rewrite a_ren_l_id, a_cat_id.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
Φ1: ogs_ctx
Γ0: C
γ: ogs_env Δ Act Φ1
e: Γ0 =[ val ]> (Δ +▶ ↓⁺ Φ1)
x: T
j: Γ0 ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: Logic.transport_r
  (fun
     refine : c_cat_view
                ((fix join_pol
                    (p : polarity)
                    (o : ogs_ctx) {struct o} :
                      C :=
                    match p with
                    | Act =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ c0 =>
                        join_pol Pas c +▶ c0
                        end
                    | Pas =>
                        fun o0 : ogs_ctx =>
                        match o0 with
                        | ∅ₓ => ∅
                        | c ▶ₓ _ =>
                        join_pol Act c
                        end
                    end o) Pas Φ1) Γ0 x
                (r_cat_r j) =>
   val
     (Δ +▶
      ctx_dom_clause_4 (@ctx_dom) Φ1 Γ0 x
        (r_cat_r j) refine) x) Heq 
  (e x j) = lookup (γ;⁻ e) (r_cat_r j)
e x j = e x j ᵥ⊛ r_emb r_id
      symmetry; apply v_var_sub.
  Qed.

Machine Strategy (Def 5.19)

We define active and passive states of the machine strategy. Active states consist of the pair of a language configuration and an active OGS assignement. Passive states consist solely of a passive OGS assignement.

  Record m_strat_act Δ (Φ : ogs_ctx) : Type := MS {
    ms_conf : conf (Δ +▶ ↓⁺Φ) ;
    ms_env : ogs_env Δ Act Φ ;
  }.
  #[global] Arguments MS {Δ Φ}.
  #[global] Arguments ms_conf {Δ Φ}.
  #[global] Arguments ms_env {Δ Φ}.

  Definition m_strat_pas Δ : psh ogs_ctx := ogs_env Δ Pas.

Next we define the action and reaction morphisms of the machine strategy. First m_strat_wrap provides the active transition given an already evaluated normal form, such that the action morphism m_strat_play only has to evaluate the active part of the state. m_strat_resp mostly is a wrapper around oapp, our analogue to the embedding from normal forms to language configurations present in the paper.

  Definition m_strat_wrap {Δ Φ} (γ : ogs_env Δ Act Φ)
     : nf _ _ (Δ +▶ ↓⁺ Φ) -> (obs∙ Δ + h_actv ogs_hg (m_strat_pas Δ) Φ) :=
      fun n =>
        match c_view_cat (nf_var n) with
        | Vcat_l i => inl (i ⋅ nf_obs n)
        | Vcat_r j => inr ((j ⋅ nf_obs n) ,' (γ ;⁻ nf_args n))
        end .

  Definition m_strat_play {Δ Φ} (ms : m_strat_act Δ Φ)
    : delay (obs∙ Δ + h_actv ogs_hg (m_strat_pas Δ) Φ)
    := fmap_delay (m_strat_wrap ms.(ms_env)) (eval ms.(ms_conf)).

  Definition m_strat_resp {Δ Φ} (γ : m_strat_pas Δ Φ)
    : h_pasv ogs_hg (m_strat_act Δ) Φ
    := fun m =>
         {| ms_conf := (ₐ↓γ _ (m_var m) ᵥ⊛ᵣ r_cat3_1) ⊙ (m_obs m)⦗r_cat_rr ᵣ⊛ a_id⦘ ;
            ms_env := γ ;⁺ |} .

These action and reaction morphisms define a coalgebra, which we now embed into the final coalgebra by looping them coinductively. This constructs the indexed interaction tree arising from starting the machine strategy at a given state.

   Definition m_strat {Δ} : m_strat_act Δ ⇒ᵢ ogs_act Δ :=
    cofix _m_strat Φ e :=
       subst_delay
         (fun r => go match r with
          | inl m        => RetF m
          | inr (x ,' p) => VisF x (fun r : ogs_e.(e_rsp) _ => _m_strat _ (m_strat_resp p r))
          end)
         (m_strat_play e).

We also provide a wrapper for the passive version of the above map.

  Definition m_stratp {Δ} : m_strat_pas Δ ⇒ᵢ ogs_pas Δ :=
    fun _ x m => m_strat _ (m_strat_resp x m).

We define the notion of equivalence on machine-strategy states given by the weak bisimilarity of the induced infinite trees. There is an active version, and a passive version, working pointwise.

  Definition m_strat_act_eqv {Δ} : relᵢ (m_strat_act Δ) (m_strat_act Δ) :=
    fun i x y => m_strat i x ≈ m_strat i y.
  Notation "x ≈ₐ y" := (m_strat_act_eqv _ x y).

  Definition m_strat_pas_eqv {Δ} : relᵢ (m_strat_pas Δ) (m_strat_pas Δ) :=
    fun i x y => forall m, m_strat_resp x m ≈ₐ m_strat_resp y m .
  Notation "x ≈ₚ y" := (m_strat_pas_eqv _ x y).

A technical lemma explaining how the infinite strategy unfolds.

  Lemma unfold_mstrat {Δ a} (x : m_strat_act Δ a) :
    m_strat a x
    ≊ subst_delay
         (fun r => go match r with
          | inl m        => RetF m
          | inr (x ,' p) => VisF x (fun r : ogs_e.(e_rsp) _ => m_strat _ (m_strat_resp p r))
          end)
         (m_strat_play x).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
m_strat a x
≊ subst_delay
    (fun
       r : (fun _ : ogs_ctx => obs ∙ Δ) a +
           {x : e_qry a & m_strat_pas Δ (g_next x)} =>
     {|
       _observe :=
         match r with
         | inl m => RetF m
         | inr (x,' p) =>
             VisF x
               (fun r0 : e_rsp x =>
                m_strat (g_next r0)
                  (m_strat_resp p r0))
         end
     |}) (m_strat_play x)
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
m_strat a x
≊ subst_delay
    (fun
       r : (fun _ : ogs_ctx => obs ∙ Δ) a +
           {x : e_qry a & m_strat_pas Δ (g_next x)} =>
     {|
       _observe :=
         match r with
         | inl m => RetF m
         | inr (x,' p) =>
             VisF x
               (fun r0 : e_rsp x =>
                m_strat (g_next r0)
                  (m_strat_resp p r0))
         end
     |}) (m_strat_play x)
    apply it_eq_unstep; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match
    match _observe (eval (ms_conf x)) with
    | RetF r => RetF (m_strat_wrap (ms_env x) r)
    | TauF t =>
        TauF (fmap_delay (m_strat_wrap (ms_env x)) t)
    | VisF e k =>
        VisF e
          (fun r : ex_falso e =>
           (fun _ : T1 => m_strat_wrap (ms_env x)) <$>
           k r)
    end
  with
  | RetF (inl m) => RetF m
  | RetF (inr (x,' p)) =>
      VisF x
        (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r0)
           (m_strat_resp p r0))
  | TauF t =>
      TauF
        (subst_delay
           (fun
              r : obs ∙ Δ +
                  {x : obs ∙ ↓⁺ a &
                  m_strat_pas Δ (a ▶ₓ m_dom x)} =>
            {|
              _observe :=
                match r with
                | inl m => RetF m
                | inr (x,' p) =>
                    VisF x
                      (fun
                        r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                       =>
                       m_strat
                        (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                        (m_strat_resp p r0))
                end
            |}) t)
  | VisF e _ =>
      match
        e
        return
          (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
      with
      end
  end
  match
    match _observe (eval (ms_conf x)) with
    | RetF r => RetF (m_strat_wrap (ms_env x) r)
    | TauF t =>
        TauF (fmap_delay (m_strat_wrap (ms_env x)) t)
    | VisF e k =>
        VisF e
          (fun r : ex_falso e =>
           (fun _ : T1 => m_strat_wrap (ms_env x)) <$>
           k r)
    end
  with
  | RetF (inl m) => RetF m
  | RetF (inr (x,' p)) =>
      VisF x
        (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r0)
           (m_strat_resp p r0))
  | TauF t =>
      TauF
        (subst_delay
           (fun
              r : obs ∙ Δ +
                  {x : obs ∙ ↓⁺ a &
                  m_strat_pas Δ (a ▶ₓ m_dom x)} =>
            {|
              _observe :=
                match r with
                | inl m => RetF m
                | inr (x,' p) =>
                    VisF x
                      (fun
                        r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                       =>
                       m_strat
                        (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                        (m_strat_resp p r0))
                end
            |}) t)
  | VisF e _ =>
      match
        e
        return
          (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
      with
      end
  end
    destruct (_observe (eval (ms_conf x))); cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match m_strat_wrap (ms_env x) r with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end
  match m_strat_wrap (ms_env x) r with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (TauF
     (subst_delay
        (fun
           r : obs ∙ Δ +
               {x : obs ∙ ↓⁺ a &
               m_strat_pas Δ (a ▶ₓ m_dom x)} =>
         {|
           _observe :=
             match r with
             | inl m => RetF m
             | inr (x,' p) =>
                 VisF x
                   (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                    =>
                    m_strat 
                      (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                      (m_strat_resp p r0))
             end
         |}) (fmap_delay (m_strat_wrap (ms_env x)) t)))
  (TauF
     (subst_delay
        (fun
           r : obs ∙ Δ +
               {x : obs ∙ ↓⁺ a &
               m_strat_pas Δ (a ▶ₓ m_dom x)} =>
         {|
           _observe :=
             match r with
             | inl m => RetF m
             | inr (x,' p) =>
                 VisF x
                   (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                    =>
                    m_strat 
                      (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                      (m_strat_resp p r0))
             end
         |}) (fmap_delay (m_strat_wrap (ms_env x)) t)))
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
q: e_qry T1_0
k: forall r : e_rsp q,
itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  (e_nxt r)
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match
    q
    return
      (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
  with
  end
  match
    q
    return
      (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
  with
  end
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match m_strat_wrap (ms_env x) r with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end
  match m_strat_wrap (ms_env x) r with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end destruct (m_strat_wrap (ms_env x) r); cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
p: obs ∙ Δ
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (RetF p) (RetF p)
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
h: h_actv ogs_hg (m_strat_pas Δ) a
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (let (x, p) := h in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
  (let (x, p) := h in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
      now econstructor.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
h: h_actv ogs_hg (m_strat_pas Δ) a
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (let (x, p) := h in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
  (let (x, p) := h in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
      destruct h; econstructor; intro.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
r: nf obs val (Δ +▶ ↓⁺ a)
x0: g_move a
m: m_strat_pas Δ (g_next x0)
r0: e_rsp x0
m_strat (a ▶ₓ m_dom x0 ▶ₓ m_dom r0)
  (m_strat_resp m r0)
≊ m_strat (a ▶ₓ m_dom x0 ▶ₓ m_dom r0)
    (m_strat_resp m r0)
      apply it_eq_t_equiv.
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (TauF
     (subst_delay
        (fun
           r : obs ∙ Δ +
               {x : obs ∙ ↓⁺ a &
               m_strat_pas Δ (a ▶ₓ m_dom x)} =>
         {|
           _observe :=
             match r with
             | inl m => RetF m
             | inr (x,' p) =>
                 VisF x
                   (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                    =>
                    m_strat 
                      (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                      (m_strat_resp p r0))
             end
         |}) (fmap_delay (m_strat_wrap (ms_env x)) t)))
  (TauF
     (subst_delay
        (fun
           r : obs ∙ Δ +
               {x : obs ∙ ↓⁺ a &
               m_strat_pas Δ (a ▶ₓ m_dom x)} =>
         {|
           _observe :=
             match r with
             | inl m => RetF m
             | inr (x,' p) =>
                 VisF x
                   (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x)
                    =>
                    m_strat 
                      (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                      (m_strat_resp p r0))
             end
         |}) (fmap_delay (m_strat_wrap (ms_env x)) t))) econstructor; apply (subst_delay_eq (RX := eq)).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
(eq ==>
 it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)) (i:=a))%signature
  (fun
     r : obs ∙ Δ +
         {x : obs ∙ ↓⁺ a &
         m_strat_pas Δ (a ▶ₓ m_dom x)} =>
   {|
     _observe :=
       match r with
       | inl m => RetF m
       | inr (x,' p) =>
           VisF x
             (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x) =>
              m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                (m_strat_resp p r0))
       end
   |})
  (fun
     r : obs ∙ Δ +
         {x : obs ∙ ↓⁺ a &
         m_strat_pas Δ (a ▶ₓ m_dom x)} =>
   {|
     _observe :=
       match r with
       | inl m => RetF m
       | inr (x,' p) =>
           VisF x
             (fun r0 : obs ∙ (↓⁻ a +▶ m_dom x) =>
              m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r0)
                (m_strat_resp p r0))
       end
   |})
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eq (fun _ : T1 => eq)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
      intros ? ? <-; apply it_eq_unstep; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
x0: (obs ∙ Δ +
 {x : obs ∙ ↓⁺ a & m_strat_pas Δ (a ▶ₓ m_dom x)})%type
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match x0 with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end
  match x0 with
  | inl m => RetF m
  | inr (x,' p) =>
      VisF x
        (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
         m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
           (m_strat_resp p r))
  end
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eq (fun _ : T1 => eq)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
      destruct x0; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
p: obs ∙ Δ
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (RetF p) (RetF p)
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
s: {x : obs ∙ ↓⁺ a & m_strat_pas Δ (a ▶ₓ m_dom x)}
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (let (x, p) := s in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
  (let (x, p) := s in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eq (fun _ : T1 => eq)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
p: obs ∙ Δ
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (RetF p) (RetF p) now econstructor.
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
s: {x : obs ∙ ↓⁺ a & m_strat_pas Δ (a ▶ₓ m_dom x)}
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  (let (x, p) := s in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r)))
  (let (x, p) := s in
   VisF x
     (fun r : obs ∙ (↓⁻ a +▶ m_dom x) =>
      m_strat (a ▶ₓ m_dom x ▶ₓ m_dom r)
        (m_strat_resp p r))) destruct s; econstructor; intro; now apply it_eq_t_equiv.
      +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
t: itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  T1_0
it_eq (fun _ : T1 => eq)
  (fmap_delay (m_strat_wrap (ms_env x)) t)
  (fmap_delay (m_strat_wrap (ms_env x)) t) now apply it_eq_t_equiv.
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
Δ: C
a: ogs_ctx
x: m_strat_act Δ a
q: e_qry T1_0
k: forall r : e_rsp q,
itree ∅ₑ (fun _ : T1 => nf obs val (Δ +▶ ↓⁺ a))
  (e_nxt r)
it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_eq (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a
  match
    q
    return
      (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
  with
  end
  match
    q
    return
      (itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a)
  with
  end destruct q.
  Qed.

Next we construct the initial states. The active initial state is given by simply a configuration from the language machine while a passive initial state is given by an assignment into the final context Δ.

   Definition inj_init_act Δ {Γ} (c : conf Γ) : m_strat_act Δ (∅ₓ ▶ₓ Γ) :=
    {| ms_conf := c ₜ⊛ᵣ (r_cat_r ᵣ⊛ r_cat_r) ; ms_env := ε⁻ ;⁺ |}.

  Definition inj_init_pas {Δ Γ} (γ : Γ =[val]> Δ) : m_strat_pas Δ (∅ₓ ▶ₓ Γ) :=
    ε⁺ ;⁻ (γ ⊛ᵣ r_cat_l).

This defines a notion of equivalence on the configurations of the language: bisimilarity of the induced strategies.

  Definition m_conf_eqv Δ : relᵢ conf conf :=
    fun Γ u v => inj_init_act Δ u ≈ₐ inj_init_act Δ v .

Finally we define composition of two matching machine-strategy states.

  Record reduce_t (Δ : C) : Type := RedT {
    red_ctx : ogs_ctx ;
    red_act : m_strat_act Δ red_ctx ;
    red_pas : m_strat_pas Δ red_ctx
  } .
  #[global] Arguments RedT {Δ Φ} u v : rename.
  #[global] Arguments red_ctx {Δ}.
  #[global] Arguments red_act {Δ}.
  #[global] Arguments red_pas {Δ}.

First the composition equation.

  Definition compo_body {Δ} (x : reduce_t Δ)
    : delay (reduce_t Δ + obs∙ Δ)
    := fmap_delay (fun r => match r with
                  | inl r => inr r
                  | inr e => inl (RedT (m_strat_resp x.(red_pas) (projT1 e)) (projT2 e))
                  end)
                  (m_strat_play x.(red_act)).

Then its naive fixpoint.

  Definition compo {Δ a} (u : m_strat_act Δ a) (v : m_strat_pas Δ a)
    : delay (obs∙ Δ)
    := iter_delay compo_body (RedT u v).
End with_param.

Finally we expose a bunch of notations to make everything more readable.

#[global] Notation "'ε⁺'" := (ENilA).
#[global] Notation "'ε⁻'" := (ENilP).
#[global] Notation "u ;⁺" := (EConA u).
#[global] Notation "u ;⁻ e" := (EConP u e).
#[global] Notation "ₐ↓ γ" := (collapse γ).
#[global] Notation "u ∥ v" := (compo u v).
#[global] Notation "x ≈ₐ y" := (m_strat_act_eqv _ x y).
#[global] Notation "x ≈ₚ y" := (m_strat_pas_eqv _ x y).
#[global] Notation "x ≈⟦ogs Δ ⟧≈ y" := (m_conf_eqv Δ _ x y).