OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedSourceSyntax.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceCellConstant line 16
  2. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceWidthConstant line 17
  3. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceCopiedConstant line 18
  4. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceExpressionConstant line 19
  5. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceRatioConstant line 20
  6. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceSurvivingSlotConstant line 21
  7. def OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceSurvivingConstant line 23
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceWidthConstant_pos line 25
  9. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.sourceCopiedConstant_pos line 29
  10. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_sourceCell_bound line 37
  11. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_survivingSourceWidthBudget line 41
  12. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_sourceWidth_le line 48
  13. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_sourceCopied_card_le line 53
  14. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_sourceSurviving_card_le line 64
  15. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_survivingSampledExpressions_syntaxSize line 86
  16. theorem OAI.Ostmann.Characters.TemplateOneSidedSourceSyntax.actual_survivingCopiedProductExpression_syntaxSize line 93