OAI/Combinatorics/VariableWL/Descriptor.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.PolyRecipe.any line 9
  2. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.any_bit line 10
  3. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachInitial line 14
  4. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachUpdate line 16
  5. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachNext line 19
  6. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachInitial_value line 22
  7. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachUpdate_bit line 28
  8. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachNext_value line 33
  9. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachInitial_length line 40
  10. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachNext_length line 44
  11. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachBody line 48
  12. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachProgram line 49
  13. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachPrefix_length line 52
  14. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachProgram_poly line 60
  15. def OAI.VariableWL.Computation.Stack.PolyRecipe.reachArray line 70
  16. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachPrefix_value line 72
  17. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.reachArray_value line 83
  18. def OAI.VariableWL.Computation.Stack.PolyRecipe.connectedProgram line 89
  19. def OAI.VariableWL.Computation.Stack.PolyRecipe.subcubicProgram line 91
  20. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.connectedProgram_bit line 94
  21. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.subcubicProgram_bit line 100
  22. def OAI.VariableWL.Computation.Stack.PolyRecipe.promiseProgram line 112
  23. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.promiseProgram_correct line 116
  24. def OAI.VariableWL.Computation.Stack.PolyRecipe.subProgram line 126
  25. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.subProgram_correct line 130
  26. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.subProgram_value line 152
  27. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.subcubic line 161
  28. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.subcubic_upper line 163
  29. def OAI.VariableWL.Computation.Stack.PolyRecipe.binaryLength line 185
  30. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binaryLength_number line 188
  31. def OAI.VariableWL.Computation.Stack.PolyRecipe.binaryDigit line 199
  32. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binaryDigit_bit line 202
  33. def OAI.VariableWL.Computation.Stack.PolyRecipe.binaryEncode line 209
  34. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binaryEncode_value line 211
  35. def OAI.VariableWL.Computation.Stack.PolyRecipe.integerEncode line 222
  36. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integerEncode_value line 225
  37. def OAI.VariableWL.Computation.Stack.PolyRecipe.graphEncode line 231
  38. def OAI.VariableWL.Computation.Stack.PolyRecipe.pairEncode line 233
  39. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.graphEncode_value line 236
  40. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.pairEncode_value line 241
  41. def OAI.VariableWL.Descriptor.rank line 253
  42. theorem OAI.VariableWL.Descriptor.rank_succ line 255
  43. theorem OAI.VariableWL.Descriptor.rank_mono line 259
  44. theorem OAI.VariableWL.Descriptor.rank_lt line 263
  45. theorem OAI.VariableWL.Descriptor.rank_exists line 268
  46. def OAI.VariableWL.Descriptor.pick line 281
  47. theorem OAI.VariableWL.Descriptor.pick_rank line 284
  48. theorem OAI.VariableWL.Descriptor.pick_spec line 298
  49. abbrev OAI.VariableWL.Descriptor.Valid line 304
  50. def OAI.VariableWL.Descriptor.rankEquiv line 306
  51. def OAI.VariableWL.Computation.Stack.PolyRecipe.underOne line 318
  52. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underOne_value line 320
  53. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underOne_bit line 326
  54. def OAI.VariableWL.Computation.Stack.PolyRecipe.select line 331
  55. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.select_number line 334
  56. def OAI.VariableWL.Computation.Stack.PolyRecipe.apply₂ line 341
  57. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.apply₂_value line 343
  58. structure OAI.VariableWL.Descriptor.Data line 352
  59. def OAI.VariableWL.Descriptor.Data.Sound line 357
  60. def OAI.VariableWL.Descriptor.Data.graph line 361
  61. def OAI.VariableWL.Descriptor.Data.iso line 377