OAI/Computability/Superstring/LexCode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.BitCode.lexLT line 7
  2. theorem OAI.Superstring.BitCode.take_eq_iff line 13
  3. theorem OAI.Superstring.BitCode.lexLT_eq line 27
  4. theorem OAI.Superstring.BitCode.poly_lexLT line 47
  5. theorem OAI.Superstring.BitCode.Poly.ltBool line 65
  6. theorem OAI.Superstring.BitCode.Poly.ltList line 72
  7. theorem OAI.Superstring.BitCode.Poly.leList line 79
  8. theorem OAI.Superstring.RotationCode.forward_mod line 93
  9. theorem OAI.Superstring.RotationCode.window_lt_iff line 100
  10. theorem OAI.Superstring.RotationCode.window_le_iff line 127
  11. def OAI.Superstring.RotationCode.phase line 133
  12. theorem OAI.Superstring.RotationCode.phase_spec line 137
  13. theorem OAI.Superstring.RotationCode.poly_phase line 174
  14. theorem OAI.Superstring.RotationCode.maximal_unique line 196
  15. theorem OAI.Superstring.RotationCode.phase_eq_distinguished line 208