OAI/Computability/DirectedFeedback/RankGraph/Store.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DirectedFeedback.StackDSL.Store line 14
  2. inductive OAI.DirectedFeedback.StackDSL.Prim line 18
  3. def OAI.DirectedFeedback.StackDSL.Prim.run line 26
  4. inductive OAI.DirectedFeedback.StackDSL.Code line 34
  5. theorem OAI.DirectedFeedback.StackDSL.Code.iterate_sum line 42
  6. def OAI.DirectedFeedback.StackDSL.Code.Label line 46
  7. instance OAI.DirectedFeedback.StackDSL.Code.labelFintype line 52
  8. def OAI.DirectedFeedback.StackDSL.Code.entry line 61
  9. def OAI.DirectedFeedback.StackDSL.Code.ret line 67
  10. theorem OAI.DirectedFeedback.StackDSL.Code.ret_eval line 72
  11. def OAI.DirectedFeedback.StackDSL.Code.primitive line 76
  12. def OAI.DirectedFeedback.StackDSL.Code.compile line 84
  13. inductive OAI.DirectedFeedback.StackDSL.Code.Exec line 107
  14. def OAI.DirectedFeedback.StackDSL.Code.cfg line 123
  15. def OAI.DirectedFeedback.StackDSL.Code.advance line 126
  16. theorem OAI.DirectedFeedback.StackDSL.Code.advance_some line 129
  17. theorem OAI.DirectedFeedback.StackDSL.Code.Exec.trace line 133
  18. def OAI.DirectedFeedback.StackDSL.Code.ioStore line 201
  19. def OAI.DirectedFeedback.StackDSL.Code.machine line 204
  20. theorem OAI.DirectedFeedback.StackDSL.Code.machine_init line 215
  21. theorem OAI.DirectedFeedback.StackDSL.Code.machine_halt line 219
  22. def OAI.DirectedFeedback.StackDSL.Code.computation line 223
  23. def OAI.DirectedFeedback.StackDSL.Store.put line 256
  24. def OAI.DirectedFeedback.StackDSL.Store.flag line 258
  25. theorem OAI.DirectedFeedback.StackDSL.Store.put_tape_same line 260
  26. theorem OAI.DirectedFeedback.StackDSL.Store.put_tape_other line 262
  27. theorem OAI.DirectedFeedback.StackDSL.Store.put_state line 264
  28. theorem OAI.DirectedFeedback.StackDSL.Store.flag_state line 266
  29. theorem OAI.DirectedFeedback.StackDSL.Store.flag_tape line 268
  30. theorem OAI.DirectedFeedback.StackDSL.Store.put_put line 269
  31. theorem OAI.DirectedFeedback.StackDSL.Store.put_self line 271
  32. theorem OAI.DirectedFeedback.StackDSL.Store.flag_flag line 275
  33. theorem OAI.DirectedFeedback.StackDSL.Store.flag_self line 277
  34. theorem OAI.DirectedFeedback.StackDSL.Store.put_flag line 278
  35. theorem OAI.DirectedFeedback.StackDSL.Store.put_comm line 281
  36. theorem OAI.DirectedFeedback.StackDSL.Store.ext line 286
  37. def OAI.DirectedFeedback.StackDSL.Ops.idle line 293
  38. def OAI.DirectedFeedback.StackDSL.Ops.reset line 294
  39. def OAI.DirectedFeedback.StackDSL.Ops.push line 295
  40. def OAI.DirectedFeedback.StackDSL.Ops.pop line 296
  41. def OAI.DirectedFeedback.StackDSL.Ops.clear line 297
  42. theorem OAI.DirectedFeedback.StackDSL.Ops.idle_run line 299
  43. theorem OAI.DirectedFeedback.StackDSL.Ops.reset_run line 302
  44. theorem OAI.DirectedFeedback.StackDSL.Ops.push_run line 305
  45. theorem OAI.DirectedFeedback.StackDSL.Ops.pop_run line 309
  46. theorem OAI.DirectedFeedback.StackDSL.Ops.clear_list line 313
  47. theorem OAI.DirectedFeedback.StackDSL.Ops.clear_run line 326
  48. def OAI.DirectedFeedback.StackDSL.Ops.transferScan line 330
  49. def OAI.DirectedFeedback.StackDSL.Ops.transfer line 331
  50. theorem OAI.DirectedFeedback.StackDSL.Ops.transferScan_run line 333
  51. theorem OAI.DirectedFeedback.StackDSL.Ops.transfer_run line 359
  52. def OAI.DirectedFeedback.StackDSL.Ops.fanScan line 367
  53. theorem OAI.DirectedFeedback.StackDSL.Ops.fanScan_run line 370
  54. def OAI.DirectedFeedback.StackDSL.Ops.copyMap line 398
  55. theorem OAI.DirectedFeedback.StackDSL.Ops.copyMap_run line 401
  56. def OAI.DirectedFeedback.StackDSL.Ops.copy line 428
  57. def OAI.DirectedFeedback.StackDSL.Ops.count line 429
  58. theorem OAI.DirectedFeedback.StackDSL.Ops.copy_run line 431
  59. theorem OAI.DirectedFeedback.StackDSL.Ops.count_run line 437
  60. theorem OAI.DirectedFeedback.StackDSL.Ops.scan_indexed line 452
  61. def OAI.DirectedFeedback.StackDSL.Ops.pushN line 475
  62. theorem OAI.DirectedFeedback.StackDSL.Ops.pushN_run line 479
  63. theorem OAI.DirectedFeedback.StackDSL.Ops.subtract_run line 488
  64. theorem OAI.DirectedFeedback.StackDSL.Ops.drop_run line 504
  65. inductive OAI.DirectedFeedback.BoundedExpr.Expr line 526
  66. def OAI.DirectedFeedback.BoundedExpr.Expr.eval line 539
  67. def OAI.DirectedFeedback.BoundedExpr.Expr.bound line 551
  68. theorem OAI.DirectedFeedback.BoundedExpr.Expr.polynomial_mono line 560
  69. theorem OAI.DirectedFeedback.BoundedExpr.Expr.eval_le_bound line 564
  70. def OAI.DirectedFeedback.BoundedExpr.Expr.compile line 607
  71. def OAI.DirectedFeedback.BoundedExpr.Expr.cost line 638
  72. def OAI.DirectedFeedback.BoundedExpr.Expr.costBound line 654
  73. theorem OAI.DirectedFeedback.BoundedExpr.Expr.cost_le_bound line 664