OAI/Computability/DirectedFeedback/RankGraph/OutputDef.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Theorem.exists_binaryGapReduction line 8
  2. theorem OAI.DFVSGames.theorem11 line 20
  3. def OAI.DirectedFeedback.BoundedExpr.Output.subst line 33
  4. theorem OAI.DirectedFeedback.BoundedExpr.Output.eval_subst line 41
  5. def OAI.DirectedFeedback.BoundedExpr.OutDef line 60
  6. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.congr line 66
  7. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.nil line 70
  8. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.bit line 71
  9. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.nat line 72
  10. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.append line 77
  11. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.const line 81
  12. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.subst line 86
  13. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.rename line 95
  14. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.loop line 98
  15. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.when line 104
  16. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.ite line 112
  17. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.flatMap line 118
  18. theorem OAI.DirectedFeedback.BoundedExpr.OutDef.finiteBind line 125
  19. abbrev OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Lit line 161
  20. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.literalBits line 163
  21. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.clauseBits line 164
  22. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.rawSplit line 166
  23. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.rawSplit_eq line 171
  24. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.literalBits_def line 195
  25. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.clauseBits_def line 201
  26. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.rawSplit_def line 206
  27. structure OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family line 233
  28. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.blockBits line 247
  29. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.eventBits line 257
  30. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.bits line 260
  31. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.blockBits_def line 265
  32. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.eventBits_def line 286
  33. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.bits_def line 289
  34. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.encodeWords_flatMap line 308
  35. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.map_finRange_val line 314
  36. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.range_flatMap line 320
  37. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.blockBits_correct line 329
  38. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.eventBits_correct line 353
  39. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.bits_correct line 360
  40. def OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.computation line 372
  41. theorem OAI.DirectedFeedback.BoundedExpr.CNFPrinter.Family.computation_finite line 380
  42. def OAI.DirectedFeedback.BoundedExpr.UnaryRead.zerosBefore line 394
  43. def OAI.DirectedFeedback.BoundedExpr.UnaryRead.word line 396
  44. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.count_eq_sum line 399
  45. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.zerosBefore_def line 409
  46. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_def line 420
  47. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_nil line 430
  48. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_true line 432
  49. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_false_zero line 439
  50. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_false_succ line 443
  51. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_prefix_zero line 450
  52. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_prefix_succ line 456
  53. theorem OAI.DirectedFeedback.BoundedExpr.UnaryRead.word_encoded line 462