OAI/Computability/DepthThree/TapeXor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DepthThreeLowerBound.TapeXor.State line 11
2. instance OAI.DepthThreeLowerBound.TapeXor.(instance at line 18) line 18
3. def OAI.DepthThreeLowerBound.TapeXor.start line 24
4. def OAI.DepthThreeLowerBound.TapeXor.done line 25
5. def OAI.DepthThreeLowerBound.TapeXor.program line 27
6. theorem OAI.DepthThreeLowerBound.TapeXor.program_done line 40
7. theorem OAI.DepthThreeLowerBound.TapeXor.step_start line 43
8. theorem OAI.DepthThreeLowerBound.TapeXor.step_scan_bit line 51
9. theorem OAI.DepthThreeLowerBound.TapeXor.step_scan_end line 62
10. theorem OAI.DepthThreeLowerBound.TapeXor.step_rewind_move line 71
11. theorem OAI.DepthThreeLowerBound.TapeXor.step_rewind_home line 79
12. theorem OAI.DepthThreeLowerBound.TapeXor.runs_scan line 87
13. theorem OAI.DepthThreeLowerBound.TapeXor.runs_rewind line 125
14. theorem OAI.DepthThreeLowerBound.TapeXor.runs_xor line 165
15. theorem OAI.DepthThreeLowerBound.TapeXor.runs_store line 192
16. theorem OAI.DepthThreeLowerBound.TapeXor.wordList_xor line 209
17. theorem OAI.DepthThreeLowerBound.TapeXor.runs_wordStore line 216