OAI/Computability/WeisfeilerLeman/Arithmetic.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.TypedStack.Code.copy line 10
  2. theorem OAI.WLTime.TypedStack.Code.copy_exec line 13
  3. def OAI.WLTime.TypedStack.Code.moveList line 35
  4. theorem OAI.WLTime.TypedStack.Code.moveList_exec line 38
  5. def OAI.WLTime.UnaryPrograms.numeral line 67
  6. def OAI.WLTime.UnaryPrograms.scan line 69
  7. def OAI.WLTime.UnaryPrograms.isTrue line 74
  8. def OAI.WLTime.UnaryPrograms.readLoop line 75
  9. def OAI.WLTime.UnaryPrograms.read line 77
  10. def OAI.WLTime.UnaryPrograms.prefixTail line 79
  11. theorem OAI.WLTime.UnaryPrograms.prefixTail_tail line 84
  12. theorem OAI.WLTime.UnaryPrograms.readLoop_exec line 89
  13. theorem OAI.WLTime.UnaryPrograms.read_exec line 133
  14. theorem OAI.WLTime.UnaryPrograms.scan_numeral line 145
  15. theorem OAI.WLTime.UnaryPrograms.scan_le line 152
  16. def OAI.WLTime.TypedStack.Code.relabel line 165
  17. theorem OAI.WLTime.TypedStack.Code.update_sum_inr line 174
  18. theorem OAI.WLTime.TypedStack.Code.relabel_inr_exec line 179
  19. def OAI.WLTime.UnaryPrograms.repeatN line 200
  20. def OAI.WLTime.UnaryPrograms.extra line 205
  21. theorem OAI.WLTime.UnaryPrograms.extra_succ_update line 207
  22. theorem OAI.WLTime.UnaryPrograms.countdown_exec line 215
  23. theorem OAI.WLTime.UnaryPrograms.repeat_exec line 240
  24. def OAI.WLTime.TypedStack.Code.liftStacks line 268
  25. theorem OAI.WLTime.TypedStack.Code.liftStacks_apply line 273
  26. theorem OAI.WLTime.TypedStack.Code.liftStacks_update line 280
  27. theorem OAI.WLTime.TypedStack.Code.liftStacks_tops line 298
  28. theorem OAI.WLTime.TypedStack.Code.relabel_exec line 303
  29. theorem OAI.WLTime.TypedStack.Code.relabel_exec_of_maps line 326
  30. structure OAI.WLTime.TypedStack.Program line 349
  31. def OAI.WLTime.TypedStack.Program.ambient line 356
  32. def OAI.WLTime.TypedStack.Program.Exec line 359
  33. def OAI.WLTime.TypedStack.Program.embed line 362
  34. theorem OAI.WLTime.TypedStack.Program.embed_injective line 365
  35. theorem OAI.WLTime.TypedStack.Program.raise_exec line 368
  36. def OAI.WLTime.TypedStack.Program.ofCode line 380
  37. theorem OAI.WLTime.TypedStack.Program.ofCode_exec line 382
  38. def OAI.WLTime.TypedStack.Program.seq line 385
  39. theorem OAI.WLTime.TypedStack.Program.seq_exec line 390
  40. def OAI.WLTime.TypedStack.Program.branch line 396
  41. theorem OAI.WLTime.TypedStack.Program.branch_true line 401
  42. theorem OAI.WLTime.TypedStack.Program.branch_false line 406
  43. def OAI.WLTime.TypedStack.Program.loop line 411
  44. theorem OAI.WLTime.TypedStack.Program.loop_false line 414
  45. theorem OAI.WLTime.TypedStack.Program.loop_true line 417
  46. def OAI.WLTime.TypedStack.Program.skip line 422
  47. def OAI.WLTime.TypedStack.Program.push line 423
  48. def OAI.WLTime.TypedStack.Program.pop line 424
  49. def OAI.WLTime.TypedStack.Program.clear line 425
  50. def OAI.WLTime.TypedStack.Program.read line 426
  51. def OAI.WLTime.TypedStack.Program.copy line 427
  52. def OAI.WLTime.TypedStack.Program.moveList line 429
  53. theorem OAI.WLTime.TypedStack.Program.skip_exec line 432
  54. theorem OAI.WLTime.TypedStack.Program.push_exec line 433
  55. theorem OAI.WLTime.TypedStack.Program.pop_exec line 435
  56. theorem OAI.WLTime.TypedStack.Program.clear_exec line 437
  57. theorem OAI.WLTime.TypedStack.Program.read_exec line 440
  58. theorem OAI.WLTime.TypedStack.Program.copy_exec line 446
  59. theorem OAI.WLTime.TypedStack.Program.moveList_exec line 453
  60. def OAI.WLTime.TypedStack.Program.merge line 461
  61. theorem OAI.WLTime.TypedStack.Program.merge_left line 466
  62. theorem OAI.WLTime.TypedStack.Program.merge_middle line 469
  63. theorem OAI.WLTime.TypedStack.Program.merge_right line 472
  64. def OAI.WLTime.TypedStack.Program.allocate line 475
  65. theorem OAI.WLTime.TypedStack.Program.local_exec line 478
  66. def OAI.WLTime.TypedStack.Program.repeatN line 491
  67. theorem OAI.WLTime.TypedStack.Program.repeat_exec line 494