OAI/Combinatorics/VariableWL/UnaryPower.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.Code.tripleStore line 8
  2. def OAI.VariableWL.Computation.Stack.Code.distribute line 11
  3. theorem OAI.VariableWL.Computation.Stack.Code.distribute_action line 16
  4. theorem OAI.VariableWL.Computation.Stack.Code.eval_distribute line 30
  5. def OAI.VariableWL.Computation.Stack.Code.duplicate line 45
  6. theorem OAI.VariableWL.Computation.Stack.Code.eval_duplicate line 48
  7. theorem OAI.VariableWL.Computation.Stack.Code.eval_length_add line 78
  8. def OAI.VariableWL.Computation.Stack.Code.multiplyAdd line 90
  9. theorem OAI.VariableWL.Computation.Stack.Code.eval_multiplyAdd line 94
  10. def OAI.VariableWL.Computation.Stack.UnaryPower.multiply line 147
  11. theorem OAI.VariableWL.Computation.Stack.UnaryPower.eval_multiply line 149
  12. def OAI.VariableWL.Computation.Stack.UnaryPower.program line 176
  13. def OAI.VariableWL.Computation.Stack.UnaryPower.time line 180
  14. theorem OAI.VariableWL.Computation.Stack.UnaryPower.eval_program line 184
  15. theorem OAI.VariableWL.Computation.Stack.UnaryPower.time_bound line 198
  16. def OAI.VariableWL.Computation.Stack.UnaryPower.store line 220
  17. theorem OAI.VariableWL.Computation.Stack.UnaryPower.store_initial line 224
  18. theorem OAI.VariableWL.Computation.Stack.UnaryPower.store_update_base line 228
  19. theorem OAI.VariableWL.Computation.Stack.UnaryPower.store_update_accumulator line 233
  20. def OAI.VariableWL.Computation.Stack.UnaryPower.setup line 238
  21. theorem OAI.VariableWL.Computation.Stack.UnaryPower.eval_setup line 240
  22. def OAI.VariableWL.Computation.Stack.UnaryPower.full line 262
  23. theorem OAI.VariableWL.Computation.Stack.UnaryPower.eval_full line 264
  24. theorem OAI.VariableWL.Computation.Stack.UnaryPower.full_bound line 272
  25. def OAI.VariableWL.Computation.Stack.UnaryPower.machine line 286
  26. def OAI.VariableWL.Computation.Stack.UnaryPower.constant line 288
  27. theorem OAI.VariableWL.Computation.Stack.UnaryPower.outputs line 290
  28. theorem OAI.VariableWL.Encoding.order_le_code_length line 305
  29. theorem OAI.VariableWL.Encoding.pair_orders line 314
  30. theorem OAI.VariableWL.RefinementSize.count_bound line 325
  31. theorem OAI.VariableWL.RefinementSize.capped_count_bound line 338
  32. theorem OAI.VariableWL.RefinementSize.array_bits_bound line 346
  33. theorem OAI.VariableWL.RefinementSize.polynomial_of_exponential line 354