OAI/Computability/Superstring/GroupBridge.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.ThreadArray.data line 9
  2. theorem OAI.Superstring.ThreadArray.poly_data line 12
  3. theorem OAI.Superstring.ThreadArray.data_represents line 18
  4. theorem OAI.Superstring.ThreadArray.data_size line 30
  5. theorem OAI.Superstring.ThreadArray.aligned_length_le line 36
  6. theorem OAI.Superstring.ThreadArray.letters_mem line 40
  7. abbrev OAI.Superstring.UpperCode.Book line 51
  8. def OAI.Superstring.UpperCode.lookup line 52
  9. def OAI.Superstring.UpperCode.upper line 53
  10. theorem OAI.Superstring.UpperCode.mem_upper line 54
  11. theorem OAI.Superstring.UpperCode.length_upper line 56
  12. theorem OAI.Superstring.UpperCode.upper_filter line 60
  13. abbrev OAI.Superstring.UpperCode.Param line 69
  14. def OAI.Superstring.UpperCode.params line 70
  15. def OAI.Superstring.UpperCode.test line 74
  16. def OAI.Superstring.UpperCode.choose line 90

    Source comment

    A foreign-text filter is deliberately separate: its equality test uses only a common product period, not a potentially unbounded infinite stream.
    def choose (D : GroupData α) (B : Book α) (ids : List ℕ) (cut M : ℕ) (t : ℤ)
    (foreign : Param → Bool) : Param :=
…

    Mentions: OAI.Superstring.UpperCode.Book, OAI.Superstring.UpperCode.foreign, OAI.Superstring.UpperCode.Param

  17. theorem OAI.Superstring.UpperCode.params_mem line 95
  18. theorem OAI.Superstring.UpperCode.choose_spec line 101
  19. theorem OAI.Superstring.UpperCode.poly_lookup line 119
  20. theorem OAI.Superstring.UpperCode.poly_upper line 121
  21. abbrev OAI.Superstring.UpperCode.ParamsInput line 124
  22. theorem OAI.Superstring.UpperCode.poly_params line 126
  23. abbrev OAI.Superstring.UpperCode.TestInput line 136
  24. instance OAI.Superstring.UpperCode.codedTestInput line 137
  25. theorem OAI.Superstring.UpperCode.poly_test line 138
  26. def OAI.Superstring.PeriodWord.different line 160
  27. theorem OAI.Superstring.PeriodWord.different_iff line 163
  28. theorem OAI.Superstring.PeriodWord.poly_different line 197
  29. def OAI.Superstring.UpperCode.foreign line 207
  30. theorem OAI.Superstring.UpperCode.supply_params line 210