OAI/Computability/DepthThree/TapeUnaryCompareScan.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.TapeUnaryCompareScan.State line 11
  2. def OAI.DepthThreeLowerBound.TapeUnaryCompareScan.result line 19
  3. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.result_succ line 22
  4. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_lt_iff line 25
  5. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_eq_iff line 30
  6. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_gt_iff line 35
  7. def OAI.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor line 45
  8. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_head_zero line 48
  9. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_head_succ line 51
  10. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_right line 54
  11. def OAI.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes line 59
  12. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_r line 63
  13. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_s line 67
  14. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_other line 71
  15. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.update_pairTapes_r line 76
  16. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.update_pairTapes_s line 82
  17. def OAI.DepthThreeLowerBound.TapeUnaryCompareScan.scanTapes line 87
  18. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.scanTapes_other line 90
  19. def OAI.DepthThreeLowerBound.TapeUnaryCompareScan.code line 95
  20. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_zero_zero line 107
  21. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_zero_succ line 114
  22. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_succ_zero line 121
  23. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_succ_succ line 128
  24. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_advanceS line 139
  25. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.runs_scan line 147
  26. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.runs_entry line 182
  27. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.runs_compare line 199
  28. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.prefix_append_left line 215
  29. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.prefix_append_right line 220
  30. theorem OAI.DepthThreeLowerBound.TapeUnaryCompareScan.step_done line 225