Alternative Definitions for LC:

This module defines LcAt k M, a more general definition of local closure. When k = 0, this is equivalent to LC, as shown in lcAt_iff_LC.

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt {Var : Type u} (k : ℕ) : Term Var → Prop

LcAt k M is satisfied when all bound indices of M are smaller than k.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.bvar i) = (i < k)
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar a) = True
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k t.abs = Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt (k + 1) t

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth {Var : Type u} : Term Var → ℕ

depth counts the maximum number of the lambdas that are enclosing variables.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.bvar i).depth = 0
• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar a).depth = 0
• (t₁.app t₂).depth = max t₁.depth t₂.depth
• t.abs.depth = t.depth + 1

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ind_on_depth {Var : Type u} (P : Term Var → Prop) (bvar : ∀ (i : ℕ), P (bvar i)) (fvar : ∀ (x : Var), P (fvar x)) (app : ∀ (M N : Term Var), P M → P N → P (M.app N)) (abs : ∀ (M : Term Var), P M → (∀ (N : Term Var), N.depth ≤ M.depth → P N) → P M.abs) (M : Term Var) : P M

@[simp]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth_openRec_fvar_eq_depth {Var : Type u} (M : Term Var) (x : Var) (i : ℕ) : (openRec i (fvar x) M).depth = M.depth

The depth of the lambda expression doesn't change by opening at i-th bound variable for some free variable.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth_open_fvar_eq_depth {Var : Type u} (M : Term Var) (x : Var) : (M.open' (fvar x)).depth = M.depth

The depth of the lambda expression doesn't change by opening for some free variable.

@[simp]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_openRec_fvar_iff_lcAt {Var : Type u} (M : Term Var) (x : Var) (i : ℕ) : LcAt i (openRec i (fvar x) M) ↔ LcAt (i + 1) M

Opening for some free variable at i-th bound variable, increments LcAt.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_open_fvar_iff_lcAt {Var : Type u} (M : Term Var) (x : Var) : LcAt 0 (M.open' (fvar x)) ↔ LcAt 1 M

Opening for some free variable is locally closed if and only if M is LcAt 1.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_iff_LC {Var : Type u} (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC

M is LcAt 0 if and only if M is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_openRec_lcAt {Var : Type u} (M N : Term Var) (i : ℕ) : LcAt i (openRec i N M) → LcAt (i + 1) M

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_abs_lc {Var : Type u} [HasFresh Var] {M N : Term Var} (hlc : (M.open' N).LC) : M.abs.LC