OAI/Combinatorics/ThinTrees/Encoding/InputArrays.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Input arrays.

  1. abbrev OAI.AlgorithmicThinTrees.InputStack.E line 14
  2. abbrev OAI.AlgorithmicThinTrees.InputStack.B line 15
  3. abbrev OAI.AlgorithmicThinTrees.InputStack.eCode line 16
  4. abbrev OAI.AlgorithmicThinTrees.InputStack.bCode line 17
  5. abbrev OAI.AlgorithmicThinTrees.InputStack.fieldsCode line 18
  6. def OAI.AlgorithmicThinTrees.InputStack.eFields line 20
  7. def OAI.AlgorithmicThinTrees.InputStack.bFields line 22
  8. lemma OAI.AlgorithmicThinTrees.InputStack.fieldsCode_flatten line 25
  9. lemma OAI.AlgorithmicThinTrees.InputStack.eFields_code line 35
  10. lemma OAI.AlgorithmicThinTrees.InputStack.bFields_code line 40
  11. abbrev OAI.AlgorithmicThinTrees.InputStack.eView line 46
  12. abbrev OAI.AlgorithmicThinTrees.InputStack.bView line 48
  13. def OAI.AlgorithmicThinTrees.InputStack.field line 51
  14. instance OAI.AlgorithmicThinTrees.InputStack.poly_field line 53
  15. def OAI.AlgorithmicThinTrees.InputStack.eNBinary line 55
  16. def OAI.AlgorithmicThinTrees.InputStack.eMBinary line 57
  17. def OAI.AlgorithmicThinTrees.InputStack.eKBinary line 59
  18. def OAI.AlgorithmicThinTrees.InputStack.bNBinary line 61
  19. def OAI.AlgorithmicThinTrees.InputStack.bPBinary line 63
  20. def OAI.AlgorithmicThinTrees.InputStack.bKBinary line 65
  21. instance OAI.AlgorithmicThinTrees.InputStack.poly_eNBinary line 67
  22. instance OAI.AlgorithmicThinTrees.InputStack.poly_eMBinary line 68
  23. instance OAI.AlgorithmicThinTrees.InputStack.poly_eKBinary line 69
  24. instance OAI.AlgorithmicThinTrees.InputStack.poly_bNBinary line 70
  25. instance OAI.AlgorithmicThinTrees.InputStack.poly_bPBinary line 71
  26. instance OAI.AlgorithmicThinTrees.InputStack.poly_bKBinary line 72
  27. lemma OAI.AlgorithmicThinTrees.InputStack.explicit_records_le line 74
  28. lemma OAI.AlgorithmicThinTrees.InputStack.graph_dimensions line 85
  29. lemma OAI.AlgorithmicThinTrees.InputStack.eM_bound line 110
  30. lemma OAI.AlgorithmicThinTrees.InputStack.eN_bound line 111
  31. lemma OAI.AlgorithmicThinTrees.InputStack.eK_bound line 115
  32. lemma OAI.AlgorithmicThinTrees.InputStack.bP_bound line 117
  33. lemma OAI.AlgorithmicThinTrees.InputStack.bN_bound line 118
  34. lemma OAI.AlgorithmicThinTrees.InputStack.poly_bounded_binary line 123
  35. def OAI.AlgorithmicThinTrees.InputStack.eN line 129
  36. def OAI.AlgorithmicThinTrees.InputStack.eM line 130
  37. def OAI.AlgorithmicThinTrees.InputStack.eK line 131
  38. def OAI.AlgorithmicThinTrees.InputStack.bN line 132
  39. def OAI.AlgorithmicThinTrees.InputStack.bP line 133
  40. instance OAI.AlgorithmicThinTrees.InputStack.poly_eN line 134
  41. instance OAI.AlgorithmicThinTrees.InputStack.poly_eM line 137
  42. instance OAI.AlgorithmicThinTrees.InputStack.poly_eK line 140
  43. instance OAI.AlgorithmicThinTrees.InputStack.poly_bN line 143
  44. instance OAI.AlgorithmicThinTrees.InputStack.poly_bP line 146
  45. lemma OAI.AlgorithmicThinTrees.InputStack.records_lookup line 150
  46. abbrev OAI.AlgorithmicThinTrees.InputStack.eEdgeCode line 158
  47. abbrev OAI.AlgorithmicThinTrees.InputStack.eeInput line 159
  48. abbrev OAI.AlgorithmicThinTrees.InputStack.eeIndex line 160
  49. abbrev OAI.AlgorithmicThinTrees.InputStack.bRecCode line 161
  50. abbrev OAI.AlgorithmicThinTrees.InputStack.brInput line 162
  51. abbrev OAI.AlgorithmicThinTrees.InputStack.brIndex line 163
  52. def OAI.AlgorithmicThinTrees.InputStack.eEndpointBinary line 165
  53. instance OAI.AlgorithmicThinTrees.InputStack.poly_eEndpointBinary line 175
  54. def OAI.AlgorithmicThinTrees.InputStack.eEndpoint line 178
  55. instance OAI.AlgorithmicThinTrees.InputStack.poly_eEndpoint line 179
  56. def OAI.AlgorithmicThinTrees.InputStack.bRecordBinary line 190
  57. instance OAI.AlgorithmicThinTrees.InputStack.poly_bRecordBinary line 197
  58. def OAI.AlgorithmicThinTrees.InputStack.bEndpointBinary line 200
  59. instance OAI.AlgorithmicThinTrees.InputStack.poly_bEndpointBinary line 203
  60. def OAI.AlgorithmicThinTrees.InputStack.bEndpoint line 206
  61. instance OAI.AlgorithmicThinTrees.InputStack.poly_bEndpoint line 207