OAI/Computability/DirectedFeedback/RankGraph/ExprLayout.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DirectedFeedback.BoundedExpr.Layout line 10
  2. def OAI.DirectedFeedback.BoundedExpr.Layout.temp line 24
  3. def OAI.DirectedFeedback.BoundedExpr.Layout.sumBody line 35
  4. structure OAI.DirectedFeedback.BoundedExpr.Layout.Ready line 50
  5. theorem OAI.DirectedFeedback.BoundedExpr.Layout.Ready.flag line 58
  6. theorem OAI.DirectedFeedback.BoundedExpr.Layout.Ready.temp line 60
  7. theorem OAI.DirectedFeedback.BoundedExpr.Layout.Ready.put line 65
  8. theorem OAI.DirectedFeedback.BoundedExpr.Layout.Ready.output line 71
  9. theorem OAI.DirectedFeedback.BoundedExpr.Layout.Ready.temp_put line 74
  10. def OAI.DirectedFeedback.BoundedExpr.Expr.Correct line 86
  11. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_lit line 91
  12. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_arg line 95
  13. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_length line 102
  14. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_add line 109
  15. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_mul line 126
  16. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_sub line 196
  17. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_sum line 239
  18. theorem OAI.DirectedFeedback.BoundedExpr.Expr.terminal_run line 329
  19. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_zero line 342
  20. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct_bit line 371
  21. theorem OAI.DirectedFeedback.BoundedExpr.Expr.correct line 419
  22. inductive OAI.DirectedFeedback.BoundedExpr.Output line 438
  23. def OAI.DirectedFeedback.BoundedExpr.Output.eval line 448
  24. def OAI.DirectedFeedback.BoundedExpr.Output.compile line 457
  25. def OAI.DirectedFeedback.BoundedExpr.Output.cost line 474
  26. def OAI.DirectedFeedback.BoundedExpr.Output.bound line 485
  27. def OAI.DirectedFeedback.BoundedExpr.Output.costBound line 493
  28. theorem OAI.DirectedFeedback.BoundedExpr.Output.length_range_flatMap line 501
  29. theorem OAI.DirectedFeedback.BoundedExpr.Output.length_le_bound line 507
  30. theorem OAI.DirectedFeedback.BoundedExpr.Output.cost_le_bound line 536
  31. def OAI.DirectedFeedback.BoundedExpr.Output.Correct line 579
  32. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_nil line 584
  33. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_bit line 588
  34. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_nat line 593
  35. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_append line 600
  36. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_when line 608
  37. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct_loop line 639
  38. theorem OAI.DirectedFeedback.BoundedExpr.Output.correct line 720