Normalization.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PureTypeSystem.RelationalExclusion line 18
Source documentation
Relational exclusion for finite profile components. This internal proposition is proved from weak normalization, not assumed in the main theorem.
```
def RelationalExclusion {S : Type u} (P : Specification S) : Prop :=
…
```
Mentions: OAI.PureTypeSystem.Specification
theorem OAI.PureTypeSystem.interfaces_of_exclusion line 26
Source documentation
All three actual candidate models are selected using the exact source case split. The exclusion interface is isolated, not hidden in a candidate law.
```
theorem interfaces_of_exclusion {S : Type u} [Fintype S] {P : Specification S}
    (Ω : ContextTower P) (hw : SystemWeaklyNormalizing P) (he : RelationalExclusion P)
    (C : Set (Set S)) (hC : IsComponent (PrimaryEdge P) C) :
    Nonempty (ComponentInterface.{u,u} Ω hw C) := by
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.RelationalExclusion, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.finite_normalization_of_exclusion line 38
theorem OAI.PureTypeSystem.normalization_of_finite_exclusion line 51
Source documentation
Finite restriction retains open contexts, annotations and every source rule. This closes the main theorem once the typed relational exclusion is proved for finite specifications. No finite-only conclusion is substituted for the main.
```
theorem normalization_of_finite_exclusion
    (exclude : ∀ (S : Type u) [Fintype S] (P : Specification S),
      SystemWeaklyNormalizing P → RelationalExclusion P)
    {S : Type u} {P : Specification S} (hw : SystemWeaklyNormalizing P) :
    SystemStronglyNormalizing P := by
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.RelationalExclusion, OAI.PureTypeSystem.SystemStronglyNormalizing
theorem OAI.PureTypeSystem.relational_exclusion line 69
Source documentation
Relational exclusion via the concrete illative encoding in the actual finite ambient context, not supplied as an axiom.
```
theorem relational_exclusion {S : Type u} [Fintype S] {P : Specification S}
    (hw : SystemWeaklyNormalizing P) : RelationalExclusion P := by
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.RelationalExclusion
theorem OAI.PureTypeSystem.weak_implies_strong line 82
Source documentation
System-wide weak normalization implies strong normalization for every PTS, including arbitrary sort types, nonfunctional rules and annotated terms.
Distinct definitions of this name: ComparatorChallenges/TypeSystemNormalization.lean:116 (same statement text; different proof or body). Qualify references as OAI.PureTypeSystem.weak_implies_strong@path.
```
theorem weak_implies_strong {S : Type u} (P : Specification S)
    (h : SystemWeaklyNormalizing P) : SystemStronglyNormalizing P :=
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.SystemStronglyNormalizing