StrongNorm

📁 Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean

Statistics

Metric	Count
Definitions Saturated, entails, entails_context, semanticMap	4
Theorems lc, multiApp, neutal_lc, sn, entails_context_cons, entails_context_empty, semanticMap_saturated, soundness, strong_norm	9
Total	13

Cslib.LambdaCalculus.LocallyNameless.Stlc

Definitions

Name	Category	Theorems
Saturated 📖	CompData	1 math math: semanticMap_saturated
entails 📖	MathDef	1 math math: soundness
entails_context 📖	MathDef	2 math math: entails_context_cons, entails_context_empty
semanticMap 📖	CompOp	1 math math: semanticMap_saturated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entails_context_cons 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Context.dom Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Env.fv Ty semanticMap entails_context	entails_context Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Ty	—	—
entails_context_empty 📖	mathematical	—	entails_context Cslib.LambdaCalculus.LocallyNameless.Untyped.Term	—	semanticMap_saturated
semanticMap_saturated 📖	mathematical	—	Saturated semanticMap	—	—
soundness 📖	mathematical	Typing	entails	—	semanticMap_saturated Saturated.multiApp Cslib.HasFresh.fresh_exists
strong_norm 📖	mathematical	Typing	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.SN	—	Saturated.sn semanticMap_saturated soundness entails_context_empty

Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lc 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated Cslib.LambdaCalculus.LocallyNameless.Untyped.Term	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LC	—	—
multiApp 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LC Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.SN Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open'	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiApp Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.app Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.abs	—	—
neutal_lc 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Neutral Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LC	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term	—	—
sn 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated Cslib.LambdaCalculus.LocallyNameless.Untyped.Term	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.SN	—	—

---

← Back to Index