OAI/Computability/DegreeRigidity/SetModels/RegularBinaryTree.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RegularBinaryTree.children line 10
  2. theorem OAI.TuringRigidity.RegularBinaryTree.children_spec line 16
  3. theorem OAI.TuringRigidity.RegularBinaryTree.children_unique line 32
  4. def OAI.TuringRigidity.RegularBinaryTree.tree line 40
  5. theorem OAI.TuringRigidity.RegularBinaryTree.tree_nil line 43
  6. theorem OAI.TuringRigidity.RegularBinaryTree.tree_append line 46
  7. theorem OAI.TuringRigidity.RegularBinaryTree.tree_positive line 61
  8. theorem OAI.TuringRigidity.RegularBinaryTree.tree_refines line 70
  9. theorem OAI.TuringRigidity.RegularBinaryTree.tree_child_subset line 77
  10. theorem OAI.TuringRigidity.RegularBinaryTree.tree_append_subset line 82
  11. theorem OAI.TuringRigidity.RegularBinaryTree.tree_prefix line 89
  12. theorem OAI.TuringRigidity.RegularBinaryTree.tree_incompatible line 93
  13. theorem OAI.TuringRigidity.RegularBinaryTree.level_overlaps line 102
  14. theorem OAI.TuringRigidity.RegularBinaryTree.refines_enumerated line 119
  15. theorem OAI.TuringRigidity.RegularBinaryTree.tree_dense line 134