OAI/Combinatorics/EditApproximation/Refinement/PhysicalSubtree.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Comparison paths below an arbitrary physical node retain their original global table labels. No refinement program or random law is changed.

  1. def OAI.EditApproximation.treeLayerAppend line 10
  2. def OAI.EditApproximation.physicalSubtreeNode line 15
  3. theorem OAI.EditApproximation.physicalSubtreeNode_zero line 19
  4. theorem OAI.EditApproximation.physicalSubtreeNode_child line 24
  5. theorem OAI.EditApproximation.comparisonSubtree_active_source line 29
  6. def OAI.EditApproximation.comparisonSubtreeLift line 46
  7. theorem OAI.EditApproximation.comparisonSubtreeLift_root line 55
  8. theorem OAI.EditApproximation.comparisonSubtreeLift_step_active line 66
  9. theorem OAI.EditApproximation.comparisonSubtreeLift_terminal line 99
  10. theorem OAI.EditApproximation.comparisonSubtreeLift_mono line 124
  11. theorem OAI.EditApproximation.comparisonSubtreeLift_bounds line 144
  12. theorem OAI.EditApproximation.comparisonSubtreeLift_gap line 175