OAI/Computability/WLIdentification/SchemaPresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLIdentification.FinitePresentation.SchemaRealizer line 10
  2. abbrev OAI.WLIdentification.FinitePresentation.SchemaRealizer.internalP line 31
  3. abbrev OAI.WLIdentification.FinitePresentation.SchemaRealizer.linkP line 32
  4. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.internalIndex line 34
  5. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.linkIndex line 40
  6. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.internalDimension line 49
  7. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.wireCode line 52
  8. theorem OAI.WLIdentification.FinitePresentation.SchemaRealizer.wireCode_eq line 55
  9. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.firstEval line 68
  10. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.secondEval line 72
  11. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.first line 77
  12. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.second line 98
  13. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.labels line 129
  14. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.matching line 149
  15. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.secondLabelEval line 160
  16. theorem OAI.WLIdentification.FinitePresentation.SchemaRealizer.secondLabelEval_eq line 163
  17. theorem OAI.WLIdentification.FinitePresentation.SchemaRealizer.mapping_poly_of line 181
  18. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.firstForm line 189
  19. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.secondForm line 215
  20. def OAI.WLIdentification.FinitePresentation.SchemaRealizer.ring line 244