Research proof index

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

If a standard reduction reaches an abstraction, then its leading Call-by-Name reduction reaches an abstraction that standardly reduces to the same target.