OAI/Computability/WeisfeilerLeman/Universal.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.OneTape.Symbolic.FullWriter.tapesBound line 9
  2. def OAI.WLTime.OneTape.Symbolic.FullWriter.alphabetBound line 10
  3. def OAI.WLTime.OneTape.Symbolic.FullWriter.statesBound line 11
  4. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.consumer_alphabet line 14
  5. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.consumer_states line 28
  6. def OAI.WLTime.Diagonal.unary line 63
  7. def OAI.WLTime.Diagonal.parseUnary line 65
  8. theorem OAI.WLTime.Diagonal.parseUnary_encode line 72
  9. def OAI.WLTime.Diagonal.moveCode line 81
  10. def OAI.WLTime.Diagonal.decodeMove line 83
  11. theorem OAI.WLTime.Diagonal.decodeMove_code line 86
  12. theorem OAI.WLTime.Diagonal.moveCode_lt line 87
  13. abbrev OAI.WLTime.Diagonal.Entry line 89
  14. structure OAI.WLTime.Diagonal.Raw line 90
  15. def OAI.WLTime.Diagonal.Raw.Valid line 96
  16. instance OAI.WLTime.Diagonal.(instance at line 100) line 100
  17. def OAI.WLTime.Diagonal.raw line 102
  18. theorem OAI.WLTime.Diagonal.raw_valid line 110
  19. def OAI.WLTime.Diagonal.Raw.machine line 117
  20. theorem OAI.WLTime.Diagonal.machine_raw line 129
  21. def OAI.WLTime.Diagonal.entryBits line 139
  22. def OAI.WLTime.Diagonal.tableBits line 140
  23. def OAI.WLTime.Diagonal.Raw.bits line 141
  24. def OAI.WLTime.Diagonal.parseEntry line 143
  25. theorem OAI.WLTime.Diagonal.parseEntry_encode line 149
  26. def OAI.WLTime.Diagonal.parseTable line 153
  27. theorem OAI.WLTime.Diagonal.parseTable_encode line 160
  28. def OAI.WLTime.Diagonal.parseRaw line 174
  29. theorem OAI.WLTime.Diagonal.parseRaw_bits line 180
  30. def OAI.WLTime.Diagonal.decode line 188
  31. def OAI.WLTime.Diagonal.description line 192
  32. theorem OAI.WLTime.Diagonal.decode_description line 194
  33. def OAI.WLTime.Diagonal.designation line 199
  34. def OAI.WLTime.Diagonal.designated line 201
  35. theorem OAI.WLTime.Diagonal.designated_prefix line 205
  36. def OAI.WLTime.Diagonal.Language line 210
  37. def OAI.WLTime.Diagonal.Decides line 213
  38. theorem OAI.WLTime.Diagonal.language_prefix line 216
  39. theorem OAI.WLTime.Diagonal.bounded_accepts_iff line 225
  40. theorem OAI.WLTime.Diagonal.prefix_time_lower line 233
  41. theorem OAI.WLTime.Diagonal.every_length line 240
  42. def OAI.WLTime.Universal.fields line 254
  43. theorem OAI.WLTime.Universal.fields_nil line 256
  44. theorem OAI.WLTime.Universal.fields_cons line 257
  45. theorem OAI.WLTime.Universal.scan_fields_cons line 261
  46. theorem OAI.WLTime.Universal.unary_tile line 264
  47. theorem OAI.WLTime.Universal.tailField_entry line 266
  48. theorem OAI.WLTime.Universal.tailField_table_drop line 272
  49. def OAI.WLTime.Universal.tile line 287
  50. theorem OAI.WLTime.Universal.fields_head line 289
  51. theorem OAI.WLTime.Universal.fields_tail line 291
  52. theorem OAI.WLTime.Universal.fields_length_le line 294
  53. inductive OAI.WLTime.Universal.Reg line 309
  54. instance OAI.WLTime.Universal.(instance at line 315) line 315
  55. def OAI.WLTime.Universal.lookup line 318
  56. theorem OAI.WLTime.Universal.scan_entry line 329
  57. theorem OAI.WLTime.Universal.scan_unary line 334
  58. theorem OAI.WLTime.Universal.table_at line 337
  59. theorem OAI.WLTime.Universal.lookup_exec line 345