OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedBudgetWindows.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Characters.TemplateOneSidedBudget.SourceWindow line 13
  2. def OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindow line 18
  3. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindow_length line 23
  4. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindow_expression line 26
  5. def OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindows line 34
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindows_length line 37
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.compileWindows_size line 46
  8. def OAI.Ostmann.Characters.TemplateOneSidedBudget.coordinateWindowExpressions line 54
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.coordinateWindowExpressions_length line 59
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.coordinateWindowExpressions_size line 64
  11. def OAI.Ostmann.Characters.TemplateOneSidedBudget.nodeWindowExpressions line 76
  12. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.nodeWindowExpressions_length line 80
  13. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.nodeWindowExpressions_size line 83
  14. def OAI.Ostmann.Characters.TemplateOneSidedBudget.candidateWindowGuards line 100
  15. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.candidateWindowGuards_length line 103
  16. theorem OAI.Ostmann.Characters.TemplateOneSidedBudget.candidateWindowGuards_size line 108