OAI/Computability/DepthThree/TapePowerCompare.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.TapePowerCompare.resultTapes_eq_frame line 12
  2. theorem OAI.DepthThreeLowerBound.TapePowerCompare.resultRegister_pair line 28
  3. theorem OAI.DepthThreeLowerBound.TapePowerCompare.resultRegister_ne line 40
  4. theorem OAI.DepthThreeLowerBound.TapePowerCompare.frame_store line 47
  5. def OAI.DepthThreeLowerBound.TapePowerCompare.outputStore line 73
  6. theorem OAI.DepthThreeLowerBound.TapePowerCompare.result_store line 77
  7. theorem OAI.DepthThreeLowerBound.TapePowerCompare.outputStore_result line 95
  8. theorem OAI.DepthThreeLowerBound.TapePowerCompare.outputStore_other line 101
  9. theorem OAI.DepthThreeLowerBound.TapePowerCompare.outputStore_clear line 107
  10. abbrev OAI.DepthThreeLowerBound.TapePowerCompare.State line 118
  11. def OAI.DepthThreeLowerBound.TapePowerCompare.program line 120
  12. def OAI.DepthThreeLowerBound.TapePowerCompare.start line 128
  13. def OAI.DepthThreeLowerBound.TapePowerCompare.done line 129
  14. def OAI.DepthThreeLowerBound.TapePowerCompare.cost line 131
  15. theorem OAI.DepthThreeLowerBound.TapePowerCompare.runs_compare line 134
  16. theorem OAI.DepthThreeLowerBound.TapePowerCompare.program_done line 169