Research proof index

Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) (lc_M : LC M.abs) : M.abs ↠ηᶠ M'.abs := by cases lc_M case abs L hL => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var rw [open_close x M 0, open_close x M' 0] all_goals...

If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then Q must be one of the following forms: Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or Q = (M ^ N) P₁ ... Pₙ

Parallel reduction has the diamond property.

The inclusion (· ⭢ₚ ·) ≤ (· ↠βᶠ ·).

A term of the form λ M N P_1 … P_n is strongly normalizing if 1. N is strongly normalizing, 1. M ^ N P₁ … Pₙ is strongly normalizing, 1. N is locally closed, 1. M ^ N P₁ … Pₙ is locally closed

An application is strongly normalizing if the left and right terms are strongly normalizing, as well as all possible future top level abstraction application beta reductions