Step subst cong r
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_subst_cong_r
Project documentation
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...
Exact Lean statement
lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
s[x := t] ↠ηᶠ s[x := t']Formal artifact
Lean source
lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) (lc_t : LC t) : s[x := t] ↠ηᶠ s[x := t'] := by induction lc_s generalizing t t' with | fvar => grind | app hl hr ih_l ih_r => trans · exact redex_app_l_cong (ih_l t t' st lc_t) (subst_lc hr lc_t) · exact redex_app_r_cong (ih_r t t' st lc_t) (subst_lc hl (step_lc_r st)) | abs L body h_lc_body ih => apply redex_abs_cong (L ∪ {x}) · intro z grind => have : (body ^ fvar z)[x := t] ↠ηᶠ (body ^ fvar z)[x := t'] finish · exact subst_lc (LC.abs L body h_lc_body) lc_t- Project
- Lean Computer Science Library
- License
- Apache-2.0
- Commit
- f36649cff2c9
- Source
- Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean:121-135
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Unique minimal
Cslib.Automata.DA.FinAcc.unique_minimal
Plain-language statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Buchi Family cover
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.
Buchi Family saturation
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Plain-language statement
na.buchiFamily saturates the ω-language accepted by na.
Source project: Lean Computer Science Library
Person-level attribution pending.