Eventual guardedness of the composition

We want to prove adequacy by unicity of solutions to the set of equations defining the composition. To do so, we rely on the notion of guarded iteration introduced in ITree/Guarded.v. Through this file, we prove that the composition is indeed eventually guarded. As described in §6.3, the proof relies crucially on the eval_app_not_var assumption (Def 6.21).

We consider a language abstractly captured as a machine satisfying an appropriate axiomatization.

  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}.
  Context {ML : machine_laws val conf obs} {VV : var_assumptions val}.

  Notation ogs_ctx := (ogs_ctx (C:=C)).

A central elements in the proof lies in ensuring that there exists a unique solution to compo_body. Since the composition of strategies is defined as such a solution, adequacy can be established by proving that evaluating and observing the substituted term is also a solution of compo_body.

By iter_evg_uniq, we know that eventually guarded equations admit a unique fixed point: we hence start by proving this eventual guardedness, captured in lemma compo_body_guarded.

This proof will among other be using an induction on the age of a variable, ie it's height in the OGS position Φ. We provide this definition and utilities.

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

  Lemma var_height_pos {Φ p x} (i : ↓[p]Φ ∋ x) : 0 < var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ogs_ctx
p: polarity
x: T
i: ↓[ p] Φ ∋ x
0 < var_height i
  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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ogs_ctx
p: polarity
x: T
i: ↓[ p] Φ ∋ x
0 < var_height i
    funelim (var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓⁻ (Φ ▶ₓ Γ) ∋ x
H: 0 < var_height i
0 < var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: 0 < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: var_height j = var_height (r_cat_l j)
0 < var_height (r_cat_l 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: 1 + c_length Φ = var_height (r_cat_r j)
0 < var_height (r_cat_r 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓⁻ (Φ ▶ₓ Γ) ∋ x
H: 0 < var_height i
0 < var_height i apply 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: 0 < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: var_height j = var_height (r_cat_l j)
0 < var_height (r_cat_l j) rewrite <- Heqcall; apply 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: 1 + c_length Φ = var_height (r_cat_r j)
0 < var_height (r_cat_r j) rewrite <- Heqcall; apply Nat.lt_0_succ.
  Qed.

  Equations lt_bound : polarity -> relation nat :=
    lt_bound Act := lt ;
    lt_bound Pas := le .

  Lemma var_height_bound {Φ p x} (i : ↓[p]Φ ∋ x)
    : lt_bound p (var_height i) (1 + c_length Φ).
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ogs_ctx
p: polarity
x: T
i: ↓[ p] Φ ∋ x
lt_bound p (var_height i) (1 + c_length Φ)
  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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ogs_ctx
p: polarity
x: T
i: ↓[ p] Φ ∋ x
lt_bound p (var_height i) (1 + c_length Φ)
    funelim (var_height i); 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓⁻ (Φ ▶ₓ Γ) ∋ x
H: lt_bound Act (var_height i) (1 + c_length Φ)
(var_height i <= S (S (c_length Φ)))%nat
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: lt_bound Pas (var_height j) (1 + c_length Φ)
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: var_height j = var_height (r_cat_l j)
var_height_clause_4 (@var_height) Φ Γ x 
  (r_cat_l j) (c_view_cat (r_cat_l j)) <
S (S (c_length Φ))
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: 1 + c_length Φ = var_height (r_cat_r j)
var_height_clause_4 (@var_height) Φ Γ x 
  (r_cat_r j) (c_view_cat (r_cat_r j)) <
S (S (c_length Φ))
    -
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓⁻ (Φ ▶ₓ Γ) ∋ x
H: lt_bound Act (var_height i) (1 + c_length Φ)
(var_height i <= S (S (c_length Φ)))%nat now apply Nat.lt_succ_r, Nat.le_le_succ_r, Nat.le_le_succ_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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: lt_bound Pas (var_height j) (1 + c_length Φ)
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Heqcall: var_height j = var_height (r_cat_l j)
var_height_clause_4 (@var_height) Φ Γ x 
  (r_cat_l j) (c_view_cat (r_cat_l j)) <
S (S (c_length Φ)) rewrite Heq; now apply Nat.lt_succ_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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Heqcall: 1 + c_length Φ = var_height (r_cat_r j)
var_height_clause_4 (@var_height) Φ Γ x 
  (r_cat_r j) (c_view_cat (r_cat_r j)) <
S (S (c_length Φ)) rewrite Heq; apply Nat.lt_succ_diag_r.
  Qed.

  Equations var_height' {Δ Φ p x} : Δ +▶ ↓[p]Φ ∋ x -> nat :=
    var_height' i with c_view_cat i := {
      | Vcat_l j := O ;
      | Vcat_r j := var_height j } .

This is the main theorem about height: if we lookup a variable in an OGS environment and obtain another variable, then this new variable is strictly lower than the first one.

  Lemma height_decrease {Δ Φ p} (v : ogs_env Δ p Φ) {x}
        (j : ↓[p^] Φ ∋ x)
        (H :  is_var (ₐ↓v _ j))
        : var_height' (is_var_get H) < var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
H: is_var (ₐ↓ v x j)
var_height' (is_var_get H) < var_height j
  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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
H: is_var (ₐ↓ v x j)
var_height' (is_var_get H) < var_height j
    revert H; rewrite lookup_collapse; intro 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
H: is_var
  (lookup v j
   ᵥ⊛ᵣ [r_cat_l, r_ctx_dom j ᵣ⊛ r_cat_r])
var_height' (is_var_get H) < var_height j
    destruct (view_is_var_ren _ _ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
H: is_var (lookup v j)
var_height'
  (is_var_get
     (ren_is_var [r_cat_l, r_ctx_dom j ᵣ⊛ r_cat_r] H)) <
var_height j
    rewrite ren_is_var_get; 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
H: is_var (lookup v j)
var_height'
  match c_view_cat (is_var_get H) with
  | Vcat_l i => r_cat_l i
  | Vcat_r j0 => r_cat_r (r_ctx_dom j x j0)
  end < var_height j
    remember (lookup v 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
v0: val (Δ +▶ ctx_dom j) x
Heqv0: v0 = lookup v j
H: is_var v0
var_height'
  match c_view_cat (is_var_get H) with
  | Vcat_l i => r_cat_l i
  | Vcat_r j0 => r_cat_r (r_ctx_dom j x j0)
  end < var_height j
    destruct H; cbn; destruct (c_view_cat 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
i: Δ ∋ x
Heqv0: a_id (r_cat_l i) = lookup v j
var_height' (r_cat_l i) < var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
j0: ctx_dom j ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v j
var_height' (r_cat_r (r_ctx_dom j x j0)) <
var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
i: Δ ∋ x
Heqv0: a_id (r_cat_l i) = lookup v j
var_height' (r_cat_l i) < var_height j unfold var_height'; rewrite c_view_cat_simpl_l; apply var_height_pos.
    -
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
j0: ctx_dom j ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v j
var_height' (r_cat_r (r_ctx_dom j x j0)) <
var_height j unfold var_height'; rewrite c_view_cat_simpl_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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
j0: ctx_dom j ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v j
var_height (r_ctx_dom j x j0) < var_height j
      remember (r_ctx_dom 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
p: polarity
v: ogs_env Δ p Φ
x: T
j: ↓[ p ^] Φ ∋ x
j0: ctx_dom j ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v j
a: ctx_dom j ⊆ ↓[ p] Φ
Heqa: a = r_ctx_dom j
var_height (a x j0) < var_height j
      funelim (r_ctx_dom j); try clear Heqcall.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓[ Act ^] (Φ ▶ₓ Γ) ∋ x
H: forall (Δ : C) (v : ogs_env Δ Pas Φ)
  (j0 : ctx_dom i ∋ x),
a_id (r_cat_r j0) = lookup v i ->
forall a : ctx_dom i ⊆ ↓⁻ Φ,
a = r_ctx_dom i ->
var_height (a x j0) < var_height i
Δ: C
v: ogs_env Δ Act (Φ ▶ₓ Γ)
j0: ctx_dom i ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v i
var_height (r_ctx_dom i x j0) < var_height 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: forall (Δ : C) (v : ogs_env Δ Act Φ)
  (j0 : ctx_dom j ∋ x),
a_id (r_cat_r j0) = lookup v j ->
forall a : ctx_dom j ⊆ ↓⁺ Φ,
a = r_ctx_dom j ->
var_height (a x j0) < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Δ: C
v: ogs_env Δ Pas (Φ ▶ₓ Γ)
j1: ctx_dom (r_cat_l j) ∋ x
Heqv0: a_id (r_cat_r j1) = lookup v (r_cat_l j)
var_height (r_ctx_dom (r_cat_l j) x j1) <
var_height (r_cat_l 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Δ: C
v: ogs_env Δ Pas (Φ ▶ₓ Γ)
j1: ctx_dom (r_cat_r j) ∋ x
Heqv0: a_id (r_cat_r j1) = lookup v (r_cat_r j)
var_height (r_ctx_dom (r_cat_r j) x j1) <
var_height (r_cat_r 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓[ Act ^] (Φ ▶ₓ Γ) ∋ x
H: forall (Δ : C) (v : ogs_env Δ Pas Φ)
  (j0 : ctx_dom i ∋ x),
a_id (r_cat_r j0) = lookup v i ->
forall a : ctx_dom i ⊆ ↓⁻ Φ,
a = r_ctx_dom i ->
var_height (a x j0) < var_height i
Δ: C
v: ogs_env Δ Act (Φ ▶ₓ Γ)
j0: ctx_dom i ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v i
var_height (r_ctx_dom i x j0) < var_height i cbn; rewrite c_view_cat_simpl_l; 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
i: ↓[ Act ^] (Φ ▶ₓ Γ) ∋ x
H: forall (Δ : C) (v : ogs_env Δ Pas Φ)
  (j0 : ctx_dom i ∋ x),
a_id (r_cat_r j0) = lookup v i ->
forall a : ctx_dom i ⊆ ↓⁻ Φ,
a = r_ctx_dom i ->
var_height (a x j0) < var_height i
Δ: C
v: ogs_env Δ Act (Φ ▶ₓ Γ)
j0: ctx_dom i ∋ x
Heqv0: a_id (r_cat_r j0) = lookup v i
var_height (r_ctx_dom i x j0) < var_height i
        dependent destruction v; now apply (H _ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: forall (Δ : C) (v : ogs_env Δ Act Φ)
  (j0 : ctx_dom j ∋ x),
a_id (r_cat_r j0) = lookup v j ->
forall a : ctx_dom j ⊆ ↓⁺ Φ,
a = r_ctx_dom j ->
var_height (a x j0) < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Δ: C
v: ogs_env Δ Pas (Φ ▶ₓ Γ)
j1: ctx_dom (r_cat_l j) ∋ x
Heqv0: a_id (r_cat_r j1) = lookup v (r_cat_l j)
var_height (r_ctx_dom (r_cat_l j) x j1) <
var_height (r_cat_l j) 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: forall (Δ : C) (v : ogs_env Δ Act Φ)
  (j0 : ctx_dom j ∋ x),
a_id (r_cat_r j0) = lookup v j ->
forall a : ctx_dom j ⊆ ↓⁺ Φ,
a = r_ctx_dom j ->
var_height (a x j0) < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Δ: C
v: ogs_env Δ Act Φ
a: Γ =[ val ]> (Δ +▶ ↓⁺ Φ)
j1: ctx_dom (r_cat_l j) ∋ x
Heqv0: a_id (r_cat_r j1) = lookup (v;⁻ a) (r_cat_l j)
var_height (r_ctx_dom (r_cat_l j) x j1) <
var_height (r_cat_l j)
        revert j1 Heqv0; cbn; rewrite Heq; cbn; intros j1 Heqv.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
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 Φ ∋ x
H: forall (Δ : C) (v : ogs_env Δ Act Φ)
  (j0 : ctx_dom j ∋ x),
a_id (r_cat_r j0) = lookup v j ->
forall a : ctx_dom j ⊆ ↓⁺ Φ,
a = r_ctx_dom j ->
var_height (a x j0) < var_height j
Heq: c_view_cat (r_cat_l j) = Vcat_l j
Δ: C
v: ogs_env Δ Act Φ
a: Γ =[ val ]> (Δ +▶ ↓⁺ Φ)
j1: ctx_dom j ∋ x
Heqv: a_id (r_cat_r j1) = lookup v j
var_height (r_ctx_dom j x j1) < var_height j
        now apply (H _ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Δ: C
v: ogs_env Δ Pas (Φ ▶ₓ Γ)
j1: ctx_dom (r_cat_r j) ∋ x
Heqv0: a_id (r_cat_r j1) = lookup v (r_cat_r j)
var_height (r_ctx_dom (r_cat_r j) x j1) <
var_height (r_cat_r j) dependent destruction v; clear Heqv0.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Φ: ctx C
Γ: C
x: T
j: Γ ∋ x
Heq: c_view_cat (r_cat_r j) = Vcat_r j
Δ: C
v: ogs_env Δ Act Φ
a: Γ =[ val ]> (Δ +▶ ↓⁺ Φ)
j1: ctx_dom (r_cat_r j) ∋ x
var_height (r_ctx_dom (r_cat_r j) x j1) <
var_height (r_cat_r j)
        revert j1; cbn; rewrite Heq; exact var_height_bound.
  Qed.

We are now ready to prove eventual guardedness. In fact the main lemma will have a slightly different statement, considering a particular kind of pair of OGS states: the ones we obtain when restarting after an interaction. As the statement is quite long we factor it in a definition first.

  Definition compo_body_guarded_aux_stmt {Δ Φ} (u : ogs_env Δ Act Φ) (v : ogs_env Δ Pas Φ)
    {x} (o : obs x) (γ : dom o =[val]> (Δ +▶ ↓⁺ Φ)) (j : ↓⁺ Φ ∋ x) : Prop
    := ev_guarded
         (fun 'T1_0 => compo_body)
         (compo_body (RedT (MS ((ₐ↓v _ j ᵥ⊛ᵣ r_cat3_1) ⊙ o⦗r_cat_rr ᵣ⊛ a_id⦘)
                               (v ;⁺))
                           (u ;⁻ γ))) .

Now the main proof.

  Lemma compo_body_guarded_aux
    {Δ Φ} (u : ogs_env Δ Act Φ) (v : ogs_env Δ Pas Φ)
    {x} (o : obs x) γ j : compo_body_guarded_aux_stmt u v o γ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
x: T
o: obs x
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
compo_body_guarded_aux_stmt u v o γ j
  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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
x: T
o: obs x
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
compo_body_guarded_aux_stmt u v o γ j

First we setup an induction on the accessibility of the current observation in the relation given by the "no-infinite redex" property.

    revert Φ u v γ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ)) 
  (j : ↓⁺ Φ ∋ x),
compo_body_guarded_aux_stmt u v o γ j
    pose (o' := (x ,' o)); change x with (projT1 o'); change o with (projT2 o').
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
o':= x,' o: {x : T & obs x}
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 o') =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 o'),
compo_body_guarded_aux_stmt u v (projT2 o') γ j
    generalize o'; clear x o o'; intro o.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
o: {x : T & obs x}
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 o) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 o),
compo_body_guarded_aux_stmt u v (projT2 o) γ j
    pose (wf := eval_app_not_var o); induction wf.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: {x : T & obs x}
H: forall y : {x : T & obs x},
head_inst_nostep y x -> Acc head_inst_nostep y
H0: forall y : {x : T & obs x},
head_inst_nostep y x ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 x) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 x),
compo_body_guarded_aux_stmt u v (projT2 x) γ j
    destruct x as [ x o ]; cbn [ projT1 projT2 ] in *.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
H: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
Acc head_inst_nostep y
H0: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ)) 
  (j : ↓⁺ Φ ∋ x),
compo_body_guarded_aux_stmt u v o γ j
    clear H; rename H0 into IHred; intros Φ u v γ 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
compo_body_guarded_aux_stmt u v o γ j

Next we setup an induction on the height of the current variable we have restarted on.

    pose (h := lt_wf (var_height j)); remember (var_height j) as n.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
n: nat
Heqn: n = var_height j
h:= lt_wf n: Acc lt n
compo_body_guarded_aux_stmt u v o γ j
    revert Φ u v γ j Heqn; induction 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
x0: nat
H: forall y : nat, y < x0 -> Acc lt y
H0: forall y : nat,
y < x0 ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ)) 
  (j : ↓⁺ Φ ∋ x),
x0 = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
    clear H; rename x0 into n, H0 into IHvar; intros Φ u v γ j Heqn.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
n: nat
IHvar: forall y : nat,
y < n ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
Heqn: n = var_height j
compo_body_guarded_aux_stmt u v o γ j

Then we case split on whether ₐ↓ v x j is a variable or not.

    unfold compo_body_guarded_aux_stmt.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
n: nat
IHvar: forall y : nat,
y < n ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
Heqn: n = var_height j
ev_guarded
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (reduce_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => reduce_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in compo_body)
  (compo_body
     {|
       red_ctx := Φ ▶ₓ dom o;
       red_act :=
         {|
           ms_conf :=
             ₐ↓ v x j ᵥ⊛ᵣ r_cat3_1 ⊙ o
             ⦗ r_cat_rr ᵣ⊛ a_id ⦘;
           ms_env := v;⁺
         |};
       red_pas := u;⁻ γ
     |})
    pose (vv := ₐ↓ v x j); fold vv.
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
n: nat
IHvar: forall y : nat,
y < n ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
Heqn: n = var_height j
vv:= ₐ↓ v x j: val (Δ +▶ ↓⁻ Φ) x
ev_guarded
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (reduce_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => reduce_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in compo_body)
  (compo_body
     {|
       red_ctx := Φ ▶ₓ dom o;
       red_act :=
         {|
           ms_conf :=
             vv ᵥ⊛ᵣ r_cat3_1 ⊙ o ⦗ r_cat_rr ᵣ⊛ a_id ⦘;
           ms_env := v;⁺
         |};
       red_pas := u;⁻ γ
     |})
    destruct (is_var_dec vv).
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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
n: nat
IHvar: forall y : nat,
y < n ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
Heqn: n = var_height j
vv:= ₐ↓ v x j: val (Δ +▶ ↓⁻ Φ) x
i: is_var vv
ev_guarded
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (reduce_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => reduce_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in compo_body)
  (compo_body
     {|
       red_ctx := Φ ▶ₓ dom o;
       red_act :=
         {|
           ms_conf :=
             vv ᵥ⊛ᵣ r_cat3_1 ⊙ o ⦗ r_cat_rr ᵣ⊛ a_id ⦘;
           ms_env := v;⁺
         |};
       red_pas := 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
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: T
o: obs x
IHred: forall y : {x : T & obs x},
head_inst_nostep y (x,' o) ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom (projT2 y) =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ projT1 y),
compo_body_guarded_aux_stmt u v (projT2 y) γ j
n: nat
IHvar: forall y : nat,
y < n ->
forall (Φ : ogs_ctx) (u : ogs_env Δ Act Φ)
  (v : ogs_env Δ Pas Φ)
  (γ : dom o =[ val ]> (Δ +▶ ↓⁺ Φ))
  (j : ↓⁺ Φ ∋ x),
y = var_height j ->
compo_body_guarded_aux_stmt u v o γ j
Φ: ogs_ctx
u: ogs_env Δ Act Φ
v: ogs_env Δ Pas Φ
γ: dom o =[ val ]> (Δ +▶ ↓⁺ Φ)
j: ↓⁺ Φ ∋ x
Heqn: n = var_height j
vv:= ₐ↓ v x j: val (Δ +▶ ↓⁻ Φ) x
t: ¬ (is_var vv)
ev_guarded
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (reduce_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => reduce_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in compo_body)
  (compo_body
     {|
       red_ctx := Φ ▶ₓ dom o;
       red_act :=
         {|
           ms_conf :=
             vv ᵥ⊛ᵣ r_cat3_1 ⊙ o ⦗ r_cat_rr ᵣ⊛ a_id ⦘;
           ms_env := v;⁺
         |};
       red_pas := u;⁻ γ
     |})