OAI/Computability/TypeSystem/Restriction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PureTypeSystem.Expr.mapSort line 13
2. theorem OAI.PureTypeSystem.Expr.mapSort_id line 20
3. theorem OAI.PureTypeSystem.Expr.mapSort_comp line 23
4. theorem OAI.PureTypeSystem.Expr.mapSort_rename line 27
5. theorem OAI.PureTypeSystem.Expr.mapSort_liftSub line 31
6. theorem OAI.PureTypeSystem.Expr.mapSort_subst line 36
7. theorem OAI.PureTypeSystem.Expr.mapSort_single line 41
8. theorem OAI.PureTypeSystem.Expr.mapSort_instantiate line 46
9. theorem OAI.PureTypeSystem.Beta.mapSort line 56
10. theorem OAI.PureTypeSystem.Reduces.mapSort line 74
11. theorem OAI.PureTypeSystem.Converts.mapSort line 83
12. theorem OAI.PureTypeSystem.Normal.mapSort line 96
13. theorem OAI.PureTypeSystem.StronglyNormalizing.of_mapSort line 119
14. theorem OAI.PureTypeSystem.WeaklyNormalizing.mapSort line 139
15. theorem OAI.PureTypeSystem.WeaklyNormalizing.of_retraction line 144
16. theorem OAI.PureTypeSystem.HasType.monotone line 155
17. theorem OAI.PureTypeSystem.HasType.mapSort line 167
18. theorem OAI.PureTypeSystem.HasType.has_axiom line 183
19. def OAI.PureTypeSystem.Specification.restrict line 200
20. def OAI.PureTypeSystem.Specification.on line 205
21. theorem OAI.PureTypeSystem.HasType.restrict_mono line 215
22. theorem OAI.PureTypeSystem.HasType.finite_support line 220
23. theorem OAI.PureTypeSystem.SystemWeaklyNormalizing.on line 268
24. theorem OAI.PureTypeSystem.HasType.finite_counterexample line 293

    Source documentation

    A non-strongly-normalizing typed term has a counterexample over a finite subspecification. No normalization conclusion for that finite PTS is assumed.

    theorem finite_counterexample (h : HasType P Γ M T) (hn : ¬ StronglyNormalizing M)
        (hw : SystemWeaklyNormalizing P) :
        ∃ D : Finset S, ∃ Γ' : List (Expr {s // s ∈ D}),
          ∃ M' T' : Expr {s // s ∈ D},
            HasType (P.on (D : Set S)) Γ' M' T' ∧ ¬ StronglyNormalizing M' ∧
              SystemWeaklyNormalizing (P.on (D : Set S)) := by
    …

    Mentions: OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.StronglyNormalizing, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr