OAI/Computability/WLIdentification/AcceptingMates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.SimpleGraph.reachable_propagate line 9
  2. theorem OAI.WLIdentification.ComparisonSchemas.shift_link_forward line 27
  3. theorem OAI.WLIdentification.ComparisonSchemas.shift_link_backward line 51
  4. theorem OAI.WLIdentification.ComparisonSchemas.shift_agreement_reachable line 75
  5. def OAI.WLIdentification.ComparisonSchemas.SameAlignment line 98
  6. theorem OAI.WLIdentification.ComparisonSchemas.alignment_link_forward line 102
  7. theorem OAI.WLIdentification.ComparisonSchemas.alignment_link_backward line 115
  8. theorem OAI.WLIdentification.ComparisonSchemas.alignment_agreement_reachable line 128
  9. def OAI.WLIdentification.ComparisonSchemas.arm line 150
  10. def OAI.WLIdentification.ComparisonSchemas.NoRealFrom line 154
  11. theorem OAI.WLIdentification.ComparisonSchemas.arm_link line 158
  12. theorem OAI.WLIdentification.ComparisonSchemas.arm_reachable line 174
  13. theorem OAI.WLIdentification.ComparisonSchemas.arm_label line 190
  14. theorem OAI.WLIdentification.ComparisonSchemas.arm_shift line 207
  15. theorem OAI.WLIdentification.RingLayout.blockStart_eq line 231
  16. theorem OAI.WLIdentification.RingLayout.representative_row line 234
  17. theorem OAI.WLIdentification.RingLayout.wrapping_names_reachable line 237
  18. theorem OAI.WLIdentification.ComparisonSchemas.wrapping_real_addresses line 253
  19. def OAI.WLIdentification.ComparisonSchemas.expressAddress line 275
  20. theorem OAI.WLIdentification.ComparisonSchemas.wrapping_internal_addresses line 278