OAI/Combinatorics/VariableWL/MatrixOutput.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.input_one_bit line 9
  2. def OAI.VariableWL.Computation.Stack.PolyRecipe.binaryStep line 12
  3. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binaryStep_value line 15
  4. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.min_double line 21
  5. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binary_fold line 27
  6. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binary_poly line 38
  7. def OAI.VariableWL.Computation.Stack.PolyRecipe.binary line 47
  8. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binary_value line 49
  9. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binary_number line 57
  10. def OAI.VariableWL.Computation.Stack.PolyRecipe.prefixStep line 63
  11. def OAI.VariableWL.Computation.Stack.PolyRecipe.prefixValue line 65
  12. def OAI.VariableWL.Computation.Stack.PolyRecipe.headCount line 70
  13. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefixValue_bound line 75
  14. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefixValue_append line 80
  15. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefixValue_reverse line 85
  16. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefixStep_value line 98
  17. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefix_fold line 109
  18. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefix_poly line 119
  19. def OAI.VariableWL.Computation.Stack.PolyRecipe.prefixLength line 130
  20. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefix_value line 132
  21. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.prefix_number line 139
  22. theorem OAI.VariableWL.Encoding.headCount_le line 148
  23. theorem OAI.VariableWL.Encoding.header_headCount line 153
  24. theorem OAI.VariableWL.Encoding.bits_nonempty line 166
  25. theorem OAI.VariableWL.Encoding.bits_last line 172
  26. theorem OAI.VariableWL.Encoding.value_positive line 184
  27. theorem OAI.VariableWL.Encoding.canonical_iff line 198
  28. def OAI.VariableWL.Computation.Stack.PolyRecipe.take line 223
  29. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.take_value line 224
  30. def OAI.VariableWL.Computation.Stack.PolyRecipe.disj line 227
  31. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.disj_bit line 228
  32. def OAI.VariableWL.Computation.Stack.PolyRecipe.canonical line 234
  33. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.canonical_bit line 236
  34. def OAI.VariableWL.Computation.Stack.PolyRecipe.afterHeader line 242
  35. def OAI.VariableWL.Computation.Stack.PolyRecipe.integerBits line 243
  36. def OAI.VariableWL.Computation.Stack.PolyRecipe.afterInteger line 244
  37. def OAI.VariableWL.Computation.Stack.PolyRecipe.integerNumber line 245
  38. def OAI.VariableWL.Computation.Stack.PolyRecipe.integerValid line 247
  39. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.afterHeader_value line 250
  40. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integerBits_value line 253
  41. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.afterInteger_value line 256
  42. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integer_spec line 260
  43. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integer_number_exact line 268
  44. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integer_success line 273
  45. theorem OAI.VariableWL.Encoding.graph_spec line 284
  46. theorem OAI.VariableWL.Encoding.matrix_exists line 304
  47. def OAI.VariableWL.Computation.Stack.PolyRecipe.matrixEntry line 314
  48. def OAI.VariableWL.Computation.Stack.PolyRecipe.matrixValid line 315
  49. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.matrixEntry_bit line 321
  50. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.matrixValid_bit line 325
  51. def OAI.VariableWL.Computation.Stack.PolyRecipe.graphMatrix line 338
  52. def OAI.VariableWL.Computation.Stack.PolyRecipe.afterGraph line 339
  53. def OAI.VariableWL.Computation.Stack.PolyRecipe.graphValid line 340
  54. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.graphMatrix_value line 342
  55. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.afterGraph_value line 345
  56. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.graph_success line 349
  57. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.graph_fields_valid line 359
  58. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.value_le_two_pow line 370
  59. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.integerBits_length line 376
  60. def OAI.VariableWL.Computation.Stack.PolyRecipe.Enough line 380
  61. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.enough_integer line 382
  62. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.afterGraph_length line 386
  63. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.enough_afterGraph line 390
  64. def OAI.VariableWL.Computation.Stack.PolyRecipe.secondWord line 393
  65. def OAI.VariableWL.Computation.Stack.PolyRecipe.dimensionWord line 394
  66. def OAI.VariableWL.Computation.Stack.PolyRecipe.pairValid line 396
  67. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.pair_success line 400
  68. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.pairValid_exists line 446