OAI/Computability/PerfectCompleteness/Decoding/LowerCutRowsLemmas.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutRows.F2 line 16
  2. def OAI.PerfectCompleteness.LowerCutRows.reconstruct line 22
  3. theorem OAI.PerfectCompleteness.LowerCutRows.selectedRows_heq_upperNode line 30
  4. theorem OAI.PerfectCompleteness.LowerCutRows.selectedRows_evaluate_step line 44
  5. theorem OAI.PerfectCompleteness.LowerCutRows.selectedRows_evaluate line 59
  6. theorem OAI.PerfectCompleteness.LowerCutRows.selectedRows_reconstruct line 78
  7. def OAI.PerfectCompleteness.LowerCutRows.selectRows line 91
  8. theorem OAI.PerfectCompleteness.LowerCutRows.selectRows_apply line 100
  9. theorem OAI.PerfectCompleteness.LowerCutRows.selectRows_surjective line 108
  10. theorem OAI.PerfectCompleteness.LowerCutRows.selectedRows_reconstruct_eq line 119
  11. abbrev OAI.PerfectCompleteness.LowerCutAssembled.F2 line 145
  12. abbrev OAI.PerfectCompleteness.LowerCutAssembled.Assembled line 151
  13. def OAI.PerfectCompleteness.LowerCutAssembled.reconstructBuckets line 156
  14. def OAI.PerfectCompleteness.LowerCutAssembled.reconstruct line 167
  15. theorem OAI.PerfectCompleteness.LowerCutAssembled.selectedRows_reconstruct line 181
  16. theorem OAI.PerfectCompleteness.LowerCutAssembled.reconstruct_splitTape line 199
  17. theorem OAI.PerfectCompleteness.LowerCutAssembled.reconstruct_assemble line 223
  18. theorem OAI.PerfectCompleteness.LowerCutAssembled.reconstruct_congr_replace line 237
  19. theorem OAI.PerfectCompleteness.LowerCutAssembled.reconstruct_congr_outside line 281
  20. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.F2 line 308
  21. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.OtherCall line 315
  22. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.ChildArrays line 321
  23. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.Complement line 324
  24. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.NativeRows line 327
  25. abbrev OAI.PerfectCompleteness.LowerCutCallSplit.Assembled line 329
  26. instance OAI.PerfectCompleteness.LowerCutCallSplit.complementFintype line 332
  27. def OAI.PerfectCompleteness.LowerCutCallSplit.complement line 334
  28. def OAI.PerfectCompleteness.LowerCutCallSplit.splitAssembled line 337
  29. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitAssembled_complement line 343
  30. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitAssembled_rows line 346
  31. theorem OAI.PerfectCompleteness.LowerCutCallSplit.complement_call line 349
  32. theorem OAI.PerfectCompleteness.LowerCutCallSplit.complement_arrays line 353
  33. def OAI.PerfectCompleteness.LowerCutCallSplit.merge line 356
  34. theorem OAI.PerfectCompleteness.LowerCutCallSplit.merge_directRow line 363
  35. theorem OAI.PerfectCompleteness.LowerCutCallSplit.merge_otherCall line 375
  36. theorem OAI.PerfectCompleteness.LowerCutCallSplit.merge_arrays line 383
  37. theorem OAI.PerfectCompleteness.LowerCutCallSplit.split_merge line 387
  38. theorem OAI.PerfectCompleteness.LowerCutCallSplit.merge_split line 398
  39. def OAI.PerfectCompleteness.LowerCutCallSplit.splitEquiv line 409
  40. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitEquiv_apply line 418
  41. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitEquiv_symm_apply line 421
  42. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitAssembled_surjective line 425
  43. theorem OAI.PerfectCompleteness.LowerCutCallSplit.splitAssembled_injective line 428
  44. theorem OAI.PerfectCompleteness.LowerCutCallSplit.complement_merge line 431
  45. theorem OAI.PerfectCompleteness.LowerCutCallSplit.selectRows_merge line 436
  46. theorem OAI.PerfectCompleteness.LowerCutCallSplit.complement_eq_iff line 441