OAI/Computability/PerfectCompleteness/Foundations/WholeCutReplayLemmas.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutReplay.F2 line 14
  2. def OAI.PerfectCompleteness.WholeCutReplay.Tape line 20
  3. def OAI.PerfectCompleteness.WholeCutReplay.erase line 33
  4. def OAI.PerfectCompleteness.WholeCutReplay.evaluate line 44
  5. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_refl_root line 69
  6. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_refl_child line 78
  7. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_step_root line 89
  8. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_step_selected line 100
  9. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_step_ordinary line 112
  10. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_erase line 124
  11. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluate_erase_of_grouped_zero line 206
  12. def OAI.PerfectCompleteness.WholeCutReplay.fullQuery line 216
  13. theorem OAI.PerfectCompleteness.WholeCutReplay.fullQuery_erase_of_grouped_zero line 222
  14. abbrev OAI.PerfectCompleteness.WholeCutReplayGrouping.F2 line 242
  15. abbrev OAI.PerfectCompleteness.WholeCutReplayGrouping.RetainedChildren line 248
  16. def OAI.PerfectCompleteness.WholeCutReplayGrouping.assemble line 254
  17. theorem OAI.PerfectCompleteness.WholeCutReplayGrouping.assemble_splitTape line 268
  18. theorem OAI.PerfectCompleteness.WholeCutReplayGrouping.evaluate_assemble_splitTape line 294
  19. theorem OAI.PerfectCompleteness.WholeCutReplayGrouping.fullQuery_assemble_splitTape line 307
  20. def OAI.PerfectCompleteness.CutSamplerReplay.retainedSum line 337
  21. theorem OAI.PerfectCompleteness.CutSamplerReplay.retainedSum_apply line 349
  22. def OAI.PerfectCompleteness.CutSamplerReplay.evaluateSpace line 358
  23. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluateSpace_apply line 368
  24. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluateSpace_val line 395
  25. theorem OAI.PerfectCompleteness.CutSamplerReplay.evaluateSpace_erase line 402
  26. theorem OAI.PerfectCompleteness.HierarchicalArrays.joint_injective line 423
  27. def OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays line 446
  28. def OAI.PerfectCompleteness.WholeCutReplay.bucketSpace line 462
  29. theorem OAI.PerfectCompleteness.WholeCutReplay.bucketSpace_apply line 471
  30. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays_step_root line 483
  31. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays_step_selected line 493
  32. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays_step_ordinary line 503
  33. theorem OAI.PerfectCompleteness.WholeCutReplay.joint_evaluateArrays_apply line 514
  34. theorem OAI.PerfectCompleteness.WholeCutReplay.joint_evaluateArrays line 586
  35. theorem OAI.PerfectCompleteness.WholeCutReplay.fullJoint_evaluateArrays line 593
  36. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays_erase line 601
  37. theorem OAI.PerfectCompleteness.WholeCutReplay.evaluateArrays_erase_of_grouped_zero line 612
  38. theorem OAI.PerfectCompleteness.WholeCutReplay.bucketSpace_erase line 622
  39. theorem OAI.PerfectCompleteness.WholeCutReplayGrouping.evaluateArrays_assemble_splitTape line 646
  40. abbrev OAI.PerfectCompleteness.WholeCutReplayTransport.F2 line 674
  41. def OAI.PerfectCompleteness.WholeCutReplayTransport.arraysTransport line 678
  42. theorem OAI.PerfectCompleteness.WholeCutReplayTransport.joint_arraysTransport line 685
  43. def OAI.PerfectCompleteness.WholeCutReplayTransport.transport line 703
  44. theorem OAI.PerfectCompleteness.WholeCutReplayTransport.evaluate_transport line 724
  45. theorem OAI.PerfectCompleteness.WholeCutReplayTransport.fullQuery_transport line 805