OAI/Computability/TypeSystem/Plain.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Actual plain observation spaces: the domain-feedback relation is well founded for the source PTS syntax and exact source graph exclusion.

  1. structure OAI.PureTypeSystem.ActualPlain.Node line 15
  2. structure OAI.PureTypeSystem.ActualPlain.Key line 21
  3. theorem OAI.PureTypeSystem.ActualPlain.Key.sorted line 36
  4. theorem OAI.PureTypeSystem.ActualPlain.Key.target_reach line 41
  5. theorem OAI.PureTypeSystem.ActualPlain.Key.open_active line 49
  6. theorem OAI.PureTypeSystem.ActualPlain.Key.domain_edge line 58
  7. def OAI.PureTypeSystem.ActualPlain.Key.target line 63
  8. def OAI.PureTypeSystem.ActualPlain.Key.domainNode line 77
  9. theorem OAI.PureTypeSystem.ActualPlain.Key.target_profile line 88
  10. theorem OAI.PureTypeSystem.ActualPlain.Key.domainNode_type line 91
  11. def OAI.PureTypeSystem.ActualPlain.schema line 95
  12. theorem OAI.PureTypeSystem.ActualPlain.Schema.target_reach line 105
  13. theorem OAI.PureTypeSystem.ActualPlain.Schema.domain_eq line 109
  14. theorem OAI.PureTypeSystem.ActualPlain.Schema.dependency_path line 118
  15. theorem OAI.PureTypeSystem.ActualPlain.Schema.dependency_reach line 129
  16. theorem OAI.PureTypeSystem.ActualPlain.Schema.dependency_negative line 134
  17. theorem OAI.PureTypeSystem.ActualPlain.Schema.dependency_drop line 144
  18. def OAI.PureTypeSystem.ActualPlain.measure line 172
  19. theorem OAI.PureTypeSystem.ActualPlain.dependency_wellFounded line 178

    Source documentation

    All domain feedback, including feedback reached after arbitrarily many continuing frames, is strictly well founded. No bound on path length is used.

    theorem dependency_wellFounded (hno : ¬ ForbiddenConfiguration P C) :
    WellFounded (schema (Ω := Ω) (C := C) hw).Dependency := by
…

    Mentions: OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.ActualPlain.schema

  20. def OAI.PureTypeSystem.ActualPlain.Space line 203

    Source documentation

    The actual (not postulated) plain observation space of every normalized plain actual type. The base parameter B is the set of candidate assignments when used by the component interpretation.

    noncomputable def Space (hno : ¬ ForbiddenConfiguration P C) (B : Type u)
    (n : Node Ω C) : Type u :=
…

    Mentions: OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.ActualPlain.Node

  21. def OAI.PureTypeSystem.ActualPlain.prefixEquiv line 207