OAI/Combinatorics/TriangleRemoval/Queries/TreeBind.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.ExposureTree.bind line 18
  2. theorem OAI.SharpTerminalLeave.ExposureTree.evaluate_bind line 22
  3. theorem OAI.SharpTerminalLeave.ExposureTree.fresh_bind line 28
  4. def OAI.SharpTerminalLeave.ExposureTree.exposeValues line 34
  5. def OAI.SharpTerminalLeave.ExposureTree.checkNone line 38
  6. def OAI.SharpTerminalLeave.trueProbability line 44
  7. def OAI.SharpTerminalLeave.falseProbability line 45
  8. theorem OAI.SharpTerminalLeave.bool_probability_sum line 47
  9. theorem OAI.SharpTerminalLeave.trueProbability_nonneg line 54
  10. theorem OAI.SharpTerminalLeave.falseProbability_nonneg line 56
  11. theorem OAI.SharpTerminalLeave.trueProbability_le_one line 58
  12. theorem OAI.SharpTerminalLeave.trueProbability_pure line 63
  13. theorem OAI.SharpTerminalLeave.falseProbability_pure line 66
  14. theorem OAI.SharpTerminalLeave.trueProbability_bind line 69
  15. theorem OAI.SharpTerminalLeave.trueProbability_bool_bind line 77
  16. theorem OAI.SharpTerminalLeave.ExposureTree.fresh_checkNone_true line 86
  17. theorem OAI.SharpTerminalLeave.ExposureTree.exposeValues_product line 94
  18. def OAI.SharpTerminalLeave.ExposureTree.exposeLabeled line 134
  19. theorem OAI.SharpTerminalLeave.ExposureTree.exposeLabeled_product line 139
  20. def OAI.SharpTerminalLeave.gridCandidates line 184
  21. def OAI.SharpTerminalLeave.gridQueryDepth line 188
  22. def OAI.SharpTerminalLeave.gridPriorities line 203
  23. def OAI.SharpTerminalLeave.gridAnswerProbability line 206
  24. theorem OAI.SharpTerminalLeave.gridAnswerProbability_step line 210
  25. theorem OAI.SharpTerminalLeave.gridAnswerProbability_zero line 250
  26. theorem OAI.SharpTerminalLeave.gridAnswerProbability_mem_unit line 256
  27. theorem OAI.SharpTerminalLeave.prod_gridCandidates line 261
  28. theorem OAI.SharpTerminalLeave.gridAnswerProbability_factor line 268
  29. def OAI.SharpTerminalLeave.gridMessage line 277
  30. theorem OAI.SharpTerminalLeave.uniform_grid_average line 281
  31. theorem OAI.SharpTerminalLeave.gridMessage_step line 293
  32. theorem OAI.SharpTerminalLeave.ExposureTree.checkNone_done_false line 309
  33. theorem OAI.SharpTerminalLeave.gridQueryDepth_threshold_zero line 317
  34. theorem OAI.SharpTerminalLeave.gridQueryDepth_stable line 325
  35. theorem OAI.SharpTerminalLeave.gridMessage_stable line 346
  36. theorem OAI.SharpTerminalLeave.gridMessage_exact line 352