OAI/Computability/WeisfeilerLeman/Digits.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.Digits.Word line 9
  2. abbrev OAI.WLTime.Digits.encode line 10
  3. def OAI.WLTime.Digits.value line 12
  4. theorem OAI.WLTime.Digits.value_zero line 14
  5. theorem OAI.WLTime.Digits.value_succ line 17
  6. def OAI.WLTime.Digits.CarryDomain line 27
  7. def OAI.WLTime.Digits.Allowed line 31
  8. theorem OAI.WLTime.Digits.allowed_iff line 34
  9. def OAI.WLTime.Digits.inc line 39
  10. def OAI.WLTime.Digits.coordinate line 41
  11. def OAI.WLTime.Digits.applyCarry line 44
  12. theorem OAI.WLTime.Digits.inc_value line 47
  13. theorem OAI.WLTime.Digits.allowed_zero line 56
  14. theorem OAI.WLTime.Digits.allowed_succ line 60
  15. theorem OAI.WLTime.Digits.apply_zero_head line 66
  16. theorem OAI.WLTime.Digits.apply_zero_tail line 70
  17. theorem OAI.WLTime.Digits.apply_succ_head line 74
  18. theorem OAI.WLTime.Digits.apply_succ_tail line 78
  19. theorem OAI.WLTime.Digits.exists_allowed line 82
  20. theorem OAI.WLTime.Digits.carry_value line 91
  21. theorem OAI.WLTime.Digits.wrap_value line 114
  22. theorem OAI.WLTime.Digits.carry_rotation line 126
  23. theorem OAI.WLTime.Digits.carry_relation line 143
  24. theorem OAI.WLTime.Digits.nonwrap_relation line 154
  25. theorem OAI.WLTime.Digits.value_eq_zero_iff line 176
  26. theorem OAI.WLTime.Digits.allowed_last_iff line 190
  27. theorem OAI.WLTime.Digits.value_last_iff line 194
  28. abbrev OAI.WLTime.ProductBox.Address line 213
  29. structure OAI.WLTime.ProductBox.Box line 215
  30. def OAI.WLTime.ProductBox.Box.Allowed line 222
  31. def OAI.WLTime.ProductBox.Box.apply line 224
  32. def OAI.WLTime.ProductBox.Box.Rel line 226
  33. def OAI.WLTime.ProductBox.Box.reverse line 228
  34. theorem OAI.WLTime.ProductBox.Box.reverse_apply_apply line 232
  35. theorem OAI.WLTime.ProductBox.Box.apply_reverse_apply line 236
  36. theorem OAI.WLTime.ProductBox.Box.reverse_allowed line 240
  37. theorem OAI.WLTime.ProductBox.Box.reverse_relation line 251
  38. def OAI.WLTime.ProductBox.Box.identity line 260
  39. theorem OAI.WLTime.ProductBox.Box.identity_rel line 264
  40. def OAI.WLTime.ProductBox.Box.product line 268
  41. theorem OAI.WLTime.ProductBox.Box.product_allowed line 272
  42. theorem OAI.WLTime.ProductBox.Box.product_apply line 277
  43. def OAI.WLTime.ProductBox.Box.carry line 283
  44. theorem OAI.WLTime.ProductBox.Box.carry_rel line 287
  45. theorem OAI.WLTime.ProductBox.Box.borrow_rel line 292
  46. abbrev OAI.WLTime.ProductBox.time line 309
  47. abbrev OAI.WLTime.ProductBox.space line 310
  48. theorem OAI.WLTime.ProductBox.append_time_space line 312
  49. theorem OAI.WLTime.ProductBox.time_append line 315
  50. theorem OAI.WLTime.ProductBox.space_append line 317
  51. def OAI.WLTime.ProductBox.addressEquiv line 320
  52. theorem OAI.WLTime.ProductBox.Box.product_relation line 328
  53. def OAI.WLTime.NatCode.Expr.choose line 346
  54. theorem OAI.WLTime.NatCode.Expr.choose_eval line 349
  55. theorem OAI.WLTime.NatCode.Expr.choose_bounded line 354
  56. def OAI.WLTime.NatCode.Expr.incCode line 369
  57. def OAI.WLTime.NatCode.Expr.decCode line 371
  58. theorem OAI.WLTime.NatCode.Expr.incCode_eval line 374
  59. theorem OAI.WLTime.NatCode.Expr.decCode_eval line 380
  60. def OAI.WLTime.ProductBox.Formula.carryDomain line 397
  61. def OAI.WLTime.ProductBox.Formula.carryCoord line 401
  62. def OAI.WLTime.ProductBox.Formula.borrowCoord line 404
  63. def OAI.WLTime.ProductBox.Formula.borrowDomain line 407
  64. theorem OAI.WLTime.ProductBox.Formula.carryDomain_correct line 410
  65. theorem OAI.WLTime.ProductBox.Formula.carryCoord_correct line 416
  66. theorem OAI.WLTime.ProductBox.Formula.borrowCoord_correct line 424
  67. theorem OAI.WLTime.ProductBox.Formula.borrowDomain_correct line 432