OAI/Combinatorics/VariableWL/ExponentialRecipe.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.PolyRecipe.maximum line 9
  2. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.maximum_number line 10
  3. def OAI.VariableWL.Computation.Stack.PolyRecipe.rawDimension line 16
  4. def OAI.VariableWL.Computation.Stack.PolyRecipe.parsedData line 17
  5. def OAI.VariableWL.Computation.Stack.PolyRecipe.StrongEnough line 25
  6. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.strong_enough line 27
  7. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.parsed_eval line 30
  8. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.parsed_good line 43
  9. def OAI.VariableWL.Computation.Stack.PolyRecipe.generalProgram line 56
  10. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.generalProgram_correct line 59
  11. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.generalProgram_value line 88
  12. theorem OAI.VariableWL.Computation.Stack.Recipe.iterate_controlled line 97
  13. theorem OAI.VariableWL.Computation.Stack.Recipe.power_prefix line 135
  14. theorem OAI.VariableWL.Computation.Stack.Recipe.outputs line 142
  15. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.exponent line 156
  16. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.size line 158
  17. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.capacity line 159
  18. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.exponent_number line 161
  19. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.capacity_value line 164
  20. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.input_le_size line 170
  21. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.envBound_size line 175
  22. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.capacity_cost line 181
  23. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.full line 193
  24. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.full_value line 195
  25. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.full_cost line 200
  26. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.environment line 213
  27. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.inEXPTIME line 215
  28. def OAI.VariableWL.Computation.Stack.ExponentialRecipe.general line 251
  29. theorem OAI.VariableWL.Computation.Stack.ExponentialRecipe.general_upper line 253
  30. def OAI.VariableWL.NumericPromise.get line 274
  31. def OAI.VariableWL.NumericPromise.pack line 275
  32. def OAI.VariableWL.NumericPromise.update line 277
  33. def OAI.VariableWL.NumericPromise.array line 279
  34. theorem OAI.VariableWL.NumericPromise.get_pack line 283
  35. theorem OAI.VariableWL.NumericPromise.get_matrix line 297
  36. theorem OAI.VariableWL.NumericPromise.array_correct line 300
  37. def OAI.VariableWL.NumericPromise.connected line 316
  38. def OAI.VariableWL.NumericPromise.subcubic line 319
  39. theorem OAI.VariableWL.NumericPromise.connected_correct line 322
  40. theorem OAI.VariableWL.NumericPromise.subcubic_correct line 327