OAI/Computability/DepthThree/TapeEncoding.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeRegister line 12
  2. abbrev OAI.DepthThreeLowerBound.TapeRegister.input line 16
  3. abbrev OAI.DepthThreeLowerBound.TapeRegister.length line 17
  4. abbrev OAI.DepthThreeLowerBound.TapeRegister.dataLength line 18
  5. abbrev OAI.DepthThreeLowerBound.TapeRegister.ringDegree line 19
  6. abbrev OAI.DepthThreeLowerBound.TapeRegister.coeffCount line 20
  7. abbrev OAI.DepthThreeLowerBound.TapeRegister.candidate line 21
  8. abbrev OAI.DepthThreeLowerBound.TapeRegister.powerTarget line 22
  9. abbrev OAI.DepthThreeLowerBound.TapeRegister.powerScratch line 23
  10. abbrev OAI.DepthThreeLowerBound.TapeRegister.requiredLength line 24
  11. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop0 line 25
  12. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop1 line 26
  13. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop2 line 27
  14. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop3 line 28
  15. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop4 line 29
  16. abbrev OAI.DepthThreeLowerBound.TapeRegister.loop5 line 30
  17. abbrev OAI.DepthThreeLowerBound.TapeRegister.dataBits line 31
  18. abbrev OAI.DepthThreeLowerBound.TapeRegister.keyBits line 32
  19. abbrev OAI.DepthThreeLowerBound.TapeRegister.polyBits line 33
  20. abbrev OAI.DepthThreeLowerBound.TapeRegister.coeffBits line 34
  21. abbrev OAI.DepthThreeLowerBound.TapeRegister.hashBits line 35
  22. abbrev OAI.DepthThreeLowerBound.TapeRegister.accumBits line 36
  23. abbrev OAI.DepthThreeLowerBound.TapeRegister.productBits line 37
  24. abbrev OAI.DepthThreeLowerBound.TapeRegister.indexA line 38
  25. abbrev OAI.DepthThreeLowerBound.TapeRegister.indexB line 39
  26. abbrev OAI.DepthThreeLowerBound.TapeRegister.indexC line 40
  27. abbrev OAI.DepthThreeLowerBound.TapeRegister.scratchA line 41
  28. abbrev OAI.DepthThreeLowerBound.TapeRegister.scratchB line 42
  29. abbrev OAI.DepthThreeLowerBound.TapeRegister.scratchC line 43
  30. abbrev OAI.DepthThreeLowerBound.TapeRegister.savedCount line 44
  31. abbrev OAI.DepthThreeLowerBound.TapeRegister.temp0 line 45
  32. abbrev OAI.DepthThreeLowerBound.TapeRegister.temp1 line 46
  33. abbrev OAI.DepthThreeLowerBound.TapeRegister.temp2 line 47
  34. inductive OAI.DepthThreeLowerBound.TapeAtom line 51
  35. abbrev OAI.DepthThreeLowerBound.TapeMark line 59
  36. abbrev OAI.DepthThreeLowerBound.TapeSymbol line 61
  37. def OAI.DepthThreeLowerBound.cleanAtom line 63
  38. def OAI.DepthThreeLowerBound.blankSymbol line 65
  39. def OAI.DepthThreeLowerBound.rawInputSymbol line 67
  40. theorem OAI.DepthThreeLowerBound.cleanAtom_atom line 69
  41. theorem OAI.DepthThreeLowerBound.cleanAtom_mark line 71
  42. theorem OAI.DepthThreeLowerBound.default_tapeSymbol line 74
  43. theorem OAI.DepthThreeLowerBound.cleanAtom_injective line 76
  44. theorem OAI.DepthThreeLowerBound.rawInputSymbol_injective line 80
  45. theorem OAI.DepthThreeLowerBound.rawInputSymbol_ne_blank line 86
  46. abbrev OAI.DepthThreeLowerBound.TapeStore line 91
  47. def OAI.DepthThreeLowerBound.tapeRegisters line 93
  48. theorem OAI.DepthThreeLowerBound.tapeRegisters_length line 95
  49. theorem OAI.DepthThreeLowerBound.mem_tapeRegisters line 98
  50. theorem OAI.DepthThreeLowerBound.tapeRegisters_nodup line 102
  51. def OAI.DepthThreeLowerBound.encodeInput line 105
  52. theorem OAI.DepthThreeLowerBound.encodeInput_length line 107
  53. def OAI.DepthThreeLowerBound.encodeBlock line 111
  54. def OAI.DepthThreeLowerBound.encodeStore line 114
  55. theorem OAI.DepthThreeLowerBound.encodeBlock_length line 117
  56. theorem OAI.DepthThreeLowerBound.encodeBlocks_length line 121
  57. theorem OAI.DepthThreeLowerBound.encodeStore_length line 129
  58. theorem OAI.DepthThreeLowerBound.encodeStore_head? line 135
  59. theorem OAI.DepthThreeLowerBound.encodeStore_ne_nil line 138
  60. theorem OAI.DepthThreeLowerBound.encodeInput_symbols line 141
  61. theorem OAI.DepthThreeLowerBound.encodeBlock_symbols line 147
  62. theorem OAI.DepthThreeLowerBound.encodeBlocks_symbols line 156
  63. theorem OAI.DepthThreeLowerBound.encodeStore_no_blank line 162
  64. theorem OAI.DepthThreeLowerBound.encodeStore_clean line 173
  65. theorem OAI.DepthThreeLowerBound.encodeStore_tail_no_home line 184