OAI/Computability/DirectedFeedback/RankGraph/StackFinite.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectedFeedback.StackDSL.Prim.support line 12
  2. def OAI.DirectedFeedback.StackDSL.Prim.restrict line 16
  3. def OAI.DirectedFeedback.StackDSL.Store.restrict line 28
  4. theorem OAI.DirectedFeedback.StackDSL.Store.restrict_update line 31
  5. theorem OAI.DirectedFeedback.StackDSL.Prim.restrict_run line 46
  6. def OAI.DirectedFeedback.StackDSL.Code.support line 58
  7. def OAI.DirectedFeedback.StackDSL.Code.restrict line 63
  8. theorem OAI.DirectedFeedback.StackDSL.Code.Exec.restrict line 74
  9. theorem OAI.DirectedFeedback.StackDSL.Code.restrict_ioStore line 98
  10. def OAI.DirectedFeedback.StackDSL.Code.supportedComputation line 106
  11. def OAI.DirectedFeedback.BoundedExpr.Output.layout line 129
  12. def OAI.DirectedFeedback.BoundedExpr.Output.program line 140
  13. def OAI.DirectedFeedback.BoundedExpr.Output.steps line 143
  14. def OAI.DirectedFeedback.BoundedExpr.Output.time line 146
  15. theorem OAI.DirectedFeedback.BoundedExpr.Output.program_run line 149
  16. theorem OAI.DirectedFeedback.BoundedExpr.Output.steps_le_time line 183
  17. def OAI.DirectedFeedback.BoundedExpr.Output.computation line 189
  18. theorem OAI.DirectedFeedback.BoundedExpr.Output.computation_alphabet line 194
  19. def OAI.DirectedFeedback.BoundedExpr.Output.realizes line 198
  20. theorem OAI.DirectedFeedback.BoundedExpr.Output.realizes_alphabet line 209
  21. def OAI.DirectedFeedback.BoundedExpr.Expr.rename line 221
  22. theorem OAI.DirectedFeedback.BoundedExpr.Expr.eval_rename line 232
  23. def OAI.DirectedFeedback.BoundedExpr.Expr.subst line 251
  24. theorem OAI.DirectedFeedback.BoundedExpr.Expr.eval_subst line 262
  25. def OAI.DirectedFeedback.BoundedExpr.Def line 285
  26. theorem OAI.DirectedFeedback.BoundedExpr.Def.congr line 291
  27. theorem OAI.DirectedFeedback.BoundedExpr.Def.lit line 295
  28. theorem OAI.DirectedFeedback.BoundedExpr.Def.arg line 296
  29. theorem OAI.DirectedFeedback.BoundedExpr.Def.length line 297
  30. theorem OAI.DirectedFeedback.BoundedExpr.Def.bit line 298
  31. theorem OAI.DirectedFeedback.BoundedExpr.Def.add line 301
  32. theorem OAI.DirectedFeedback.BoundedExpr.Def.mul line 304
  33. theorem OAI.DirectedFeedback.BoundedExpr.Def.sub line 307
  34. theorem OAI.DirectedFeedback.BoundedExpr.Def.zero line 310
  35. theorem OAI.DirectedFeedback.BoundedExpr.Def.rename line 314
  36. theorem OAI.DirectedFeedback.BoundedExpr.Def.subst line 318
  37. theorem OAI.DirectedFeedback.BoundedExpr.Def.sum line 328
  38. theorem OAI.DirectedFeedback.BoundedExpr.Def.eq line 333
  39. theorem OAI.DirectedFeedback.BoundedExpr.Def.le line 341
  40. theorem OAI.DirectedFeedback.BoundedExpr.Def.lt line 346
  41. theorem OAI.DirectedFeedback.BoundedExpr.Def.ite line 351
  42. theorem OAI.DirectedFeedback.BoundedExpr.Def.pow line 357
  43. theorem OAI.DirectedFeedback.BoundedExpr.Def.poly line 362
  44. theorem OAI.DirectedFeedback.BoundedExpr.Def.finset_sum line 367
  45. theorem OAI.DirectedFeedback.BoundedExpr.Def.table line 375
  46. theorem OAI.DirectedFeedback.BoundedExpr.Def.div line 402
  47. theorem OAI.DirectedFeedback.BoundedExpr.Def.mod line 431
  48. theorem OAI.DirectedFeedback.BoundedExpr.Def.min line 436
  49. theorem OAI.DirectedFeedback.BoundedExpr.Def.max line 441
  50. def OAI.DirectedFeedback.BoundedExpr.FDef line 454
  51. theorem OAI.DirectedFeedback.BoundedExpr.FDef.congr line 460
  52. theorem OAI.DirectedFeedback.BoundedExpr.FDef.const line 466
  53. theorem OAI.DirectedFeedback.BoundedExpr.FDef.rename line 470
  54. theorem OAI.DirectedFeedback.BoundedExpr.FDef.subst line 473
  55. theorem OAI.DirectedFeedback.BoundedExpr.FDef.bind line 477
  56. theorem OAI.DirectedFeedback.BoundedExpr.FDef.map line 489
  57. theorem OAI.DirectedFeedback.BoundedExpr.FDef.toDef line 492
  58. theorem OAI.DirectedFeedback.BoundedExpr.FDef.ite line 500
  59. theorem OAI.DirectedFeedback.BoundedExpr.FDef.bool line 507
  60. theorem OAI.DirectedFeedback.BoundedExpr.FDef.decide line 520
  61. theorem OAI.DirectedFeedback.BoundedExpr.FDef.ofNat line 525
  62. theorem OAI.DirectedFeedback.BoundedExpr.FDef.pair line 534
  63. theorem OAI.DirectedFeedback.BoundedExpr.FDef.pi line 539
  64. def OAI.DirectedFeedback.BoundedExpr.PDef line 564
  65. theorem OAI.DirectedFeedback.BoundedExpr.PDef.congr line 570
  66. theorem OAI.DirectedFeedback.BoundedExpr.PDef.const line 573
  67. theorem OAI.DirectedFeedback.BoundedExpr.PDef.not line 576
  68. theorem OAI.DirectedFeedback.BoundedExpr.PDef.and line 581
  69. theorem OAI.DirectedFeedback.BoundedExpr.PDef.or line 586
  70. theorem OAI.DirectedFeedback.BoundedExpr.PDef.imp line 589
  71. theorem OAI.DirectedFeedback.BoundedExpr.PDef.all line 592
  72. theorem OAI.DirectedFeedback.BoundedExpr.PDef.exists_fin line 602
  73. theorem OAI.DirectedFeedback.BoundedExpr.PDef.eq line 606
  74. theorem OAI.DirectedFeedback.BoundedExpr.PDef.nat_eq line 610
  75. theorem OAI.DirectedFeedback.BoundedExpr.PDef.le line 613
  76. theorem OAI.DirectedFeedback.BoundedExpr.PDef.lt line 616
  77. theorem OAI.DirectedFeedback.BoundedExpr.PDef.decide line 619
  78. theorem OAI.DirectedFeedback.BoundedExpr.PDef.ite line 621
  79. theorem OAI.DirectedFeedback.BoundedExpr.PDef.nite line 627
  80. theorem OAI.DirectedFeedback.BoundedExpr.FDef.select line 638
  81. theorem OAI.DirectedFeedback.BoundedExpr.FDef.bool_true line 643
  82. def OAI.DirectedFeedback.DigitCodec.encode line 657
  83. def OAI.DirectedFeedback.DigitCodec.decode line 661
  84. theorem OAI.DirectedFeedback.DigitCodec.decode_lt line 665
  85. theorem OAI.DirectedFeedback.DigitCodec.encode_lt line 673
  86. theorem OAI.DirectedFeedback.DigitCodec.decode_encode line 683
  87. theorem OAI.DirectedFeedback.DigitCodec.encode_decode line 697
  88. def OAI.DirectedFeedback.DigitCodec.equiv line 708
  89. theorem OAI.DirectedFeedback.DigitCodec.decode_def line 717
  90. abbrev OAI.DirectedFeedback.BoxCodec.Box line 739
  91. def OAI.DirectedFeedback.BoxCodec.size line 740
  92. def OAI.DirectedFeedback.BoxCodec.equiv line 741
  93. def OAI.DirectedFeedback.BoxCodec.tag line 746
  94. def OAI.DirectedFeedback.BoxCodec.digits line 749
  95. def OAI.DirectedFeedback.BoxCodec.copy line 750
  96. theorem OAI.DirectedFeedback.BoxCodec.tag_equiv line 752
  97. theorem OAI.DirectedFeedback.BoxCodec.digits_equiv line 761
  98. theorem OAI.DirectedFeedback.BoxCodec.copy_equiv line 768
  99. theorem OAI.DirectedFeedback.BoxCodec.decode_tag line 773
  100. theorem OAI.DirectedFeedback.BoxCodec.decode_digits line 777
  101. theorem OAI.DirectedFeedback.BoxCodec.decode_copy line 781
  102. theorem OAI.DirectedFeedback.BoxCodec.tag_def line 786
  103. theorem OAI.DirectedFeedback.BoxCodec.digits_def line 790
  104. theorem OAI.DirectedFeedback.BoxCodec.copy_def line 794