OAI/NumberTheory/Ostmann/Construction/ScheduledTreeBulkCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The counted bulk slots are the actual recursive arithmetic leaves

  1. def OAI.Ostmann.treeLeafPathEquiv line 12
  2. def OAI.Ostmann.treeLeafEnumeration line 16
  3. theorem OAI.Ostmann.scheduledPathEnumeration_treeLeafEnumeration line 19
  4. def OAI.Ostmann.scheduledTreeBulkCoordinates line 24
  5. theorem OAI.Ostmann.scheduledTreeBulkCoordinates_leaf line 31
  6. def OAI.Ostmann.scheduledTreeBulkMatching line 40
  7. theorem OAI.Ostmann.separatedMatchingLeft_apply line 47
  8. theorem OAI.Ostmann.scheduledSplitHCoordinates_inl line 55
  9. theorem OAI.Ostmann.scheduledBulkMatching_slot line 60
  10. theorem OAI.Ostmann.scheduledTreeBulkMatching_slot line 72
  11. theorem OAI.Ostmann.scheduledTreeBulkMatching_symm_slot line 85
  12. theorem OAI.Ostmann.scheduledTreeBulkMatching_good line 95