OAI/Computability/PerfectCompleteness/Foundations/WholeArrayInteriorExteriorLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode line 17
  2. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode_refl line 21
  3. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode_step line 25
  4. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode_height line 28
  5. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode_spec line 33
  6. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperNode_path_heq line 42
  7. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.selectedNode line 46
  8. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.selectedNode_succ line 50
  9. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.selectedNode_step line 53
  10. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.selectedNode_nodePath line 60
  11. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.upperTape line 70
  12. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.read line 79
  13. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.read_split line 87
  14. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.rebuild line 95
  15. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.evaluate_rebuild_read line 103
  16. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.evaluate_rebuild_split line 153
  17. abbrev OAI.PerfectCompleteness.WholeArrayInteriorExterior.NonUpper line 165
  18. def OAI.PerfectCompleteness.WholeArrayInteriorExterior.nodeArray line 168
  19. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.nodeArray_read line 177
  20. theorem OAI.PerfectCompleteness.WholeArrayInteriorExterior.nodeArray_split line 185
  21. def OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows line 209
  22. def OAI.PerfectCompleteness.SelectedArrayReplacement.replace line 214
  23. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows_refl line 227
  24. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows_step line 231
  25. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.replace_step line 237
  26. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows_assemble_refl line 246
  27. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows_assemble_step line 253
  28. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.replace_assemble_refl line 265
  29. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.replace_assemble_step line 274
  30. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.selectedRows_replace line 289
  31. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.replace_outside line 305
  32. theorem OAI.PerfectCompleteness.SelectedArrayReplacement.replace_same line 337