OAI/Combinatorics/EditApproximation/Geometry/StateDomain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual finite labeled state type

Physical nodes are retained as depth/path pairs. In particular, repeated empty intervals remain distinct entries of the seed and refinement tables.

  1. theorem OAI.EditApproximation.targetInterval_card_le line 22
  2. abbrev OAI.EditApproximation.LabeledEntry line 30
  3. def OAI.EditApproximation.entrySourceInterval line 33
  4. def OAI.EditApproximation.entrySource line 36
  5. def OAI.EditApproximation.entryTarget line 40
  6. theorem OAI.EditApproximation.physicalNode_card line 44
  7. theorem OAI.EditApproximation.labeledEntry_card_le line 53
  8. theorem OAI.EditApproximation.computed_labeledEntry_card_le line 58
  9. theorem OAI.EditApproximation.entrySource_length_le line 63
  10. theorem OAI.EditApproximation.entryTarget_length_le line 68