OAI/NumberTheory/Ostmann/Arithmetic/HistoryHeightBudgetCost.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.product_heightCost line 13
  2. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.pivot_heightCost line 23
  3. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.slotCost line 35
  4. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.stateCost line 37
  5. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.slotCost_reorder line 40
  6. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.slotCost_append line 44
  7. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.slotCost_parts line 53
  8. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.sum_heightCost_ofFn line 60
  9. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.pivotExpr_heightCost line 68
  10. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.child_cost_le line 81
  11. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.TreeHeightCostLe line 94
  12. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.treeCostLe_mono line 99
  13. def OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.internalCost line 106
  14. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.internalCost_node line 109
  15. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.encode_cost_le line 118
  16. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.symbolicHistory_cost_le line 145
  17. theorem OAI.Ostmann.Arithmetic.HistoryHeightBudgetCost.coefficientHistory_cost_le line 156