OAI/NumberTheory/Ostmann/Arithmetic/HistorySymbolicCost.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistorySymbolicCost.slotCost line 12
  2. def OAI.Ostmann.Arithmetic.HistorySymbolicCost.stateCost line 14
  3. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.slotCost_reorder line 17
  4. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.slotCost_append line 21
  5. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.slotCost_parts line 30
  6. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.sum_atomCount_ofFn line 37
  7. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.pivotExpr_atomCount line 45
  8. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.child_cost_le line 58
  9. def OAI.Ostmann.Arithmetic.HistorySymbolicCost.TreeCostLe line 71
  10. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.treeCostLe_mono line 76
  11. def OAI.Ostmann.Arithmetic.HistorySymbolicCost.internalCost line 83
  12. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.internalCost_node line 86
  13. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.encode_cost_le line 95
  14. theorem OAI.Ostmann.Arithmetic.HistorySymbolicCost.symbolicHistory_cost_le line 123