Project-declaredLean 4.33.0-rc1
Invert abs multi App st
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.invert_abs_multiApp_st
Plain-language statement
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ā
computer sciencecomputabilityprogram semantics
Source project: Lean Computer Science Library
Person-level attribution pending.