OAI/Computability/PerfectCompleteness/Sampling/MetadataFreeSampler.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.SignTuple line 16
  2. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.EncodedAssignment line 19
  3. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.SignedLeaf line 24
  4. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.SignedDomain line 27
  5. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.SignedH line 29
  6. def OAI.PerfectCompleteness.MetadataFreeSampler.nodeSigns line 33
  7. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.SignedArrays line 37
  8. def OAI.PerfectCompleteness.MetadataFreeSampler.assignmentEquiv line 40
  9. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.ArrayTables line 45
  10. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.Input line 49
  11. instance OAI.PerfectCompleteness.MetadataFreeSampler.inputFintype line 52
  12. def OAI.PerfectCompleteness.MetadataFreeSampler.tableJoint line 57
  13. def OAI.PerfectCompleteness.MetadataFreeSampler.sourceSigns line 65
  14. abbrev OAI.PerfectCompleteness.MetadataFreeSampler.sourceSlots line 69
  15. theorem OAI.PerfectCompleteness.MetadataFreeSampler.sourceLeaf_eq line 73
  16. theorem OAI.PerfectCompleteness.MetadataFreeSampler.sourceDomain_eq line 77
  17. theorem OAI.PerfectCompleteness.MetadataFreeSampler.sourceH_eq line 81
  18. theorem OAI.PerfectCompleteness.MetadataFreeSampler.sourceNodeH_eq line 85
  19. theorem OAI.PerfectCompleteness.MetadataFreeSampler.sourceArrays_eq line 90
  20. def OAI.PerfectCompleteness.MetadataFreeSampler.sourceAssignmentEquiv line 94
  21. def OAI.PerfectCompleteness.MetadataFreeSampler.numberedAssignmentEquiv line 99
  22. def OAI.PerfectCompleteness.MetadataFreeSampler.encodeArrays line 106
  23. theorem OAI.PerfectCompleteness.MetadataFreeSampler.tableJoint_encodeArrays line 111
  24. theorem OAI.PerfectCompleteness.MetadataFreeSampler.tableJoint_at_assignment line 117
  25. theorem OAI.PerfectCompleteness.MetadataFreeSampler.numberedFunction_eq line 124
  26. def OAI.PerfectCompleteness.MetadataFreeSampler.encodeInput line 133
  27. def OAI.PerfectCompleteness.MetadataFreeSampler.encodeTape line 138
  28. theorem OAI.PerfectCompleteness.MetadataFreeSampler.numberedFunction_encodeTape line 145
  29. def OAI.PerfectCompleteness.MetadataFreeSampler.outputEquiv line 156
  30. def OAI.PerfectCompleteness.MetadataFreeSampler.numberedShapes line 160
  31. def OAI.PerfectCompleteness.MetadataFreeSampler.dummyTreeSlots line 165
  32. def OAI.PerfectCompleteness.MetadataFreeSampler.dummyNumberedEquiv line 169
  33. def OAI.PerfectCompleteness.MetadataFreeSampler.shapeInput line 174
  34. theorem OAI.PerfectCompleteness.MetadataFreeSampler.shapeInput_encodeInput line 186
  35. theorem OAI.PerfectCompleteness.MetadataFreeSampler.shapeInput_partition line 203
  36. theorem OAI.PerfectCompleteness.MetadataFreeSampler.shapeInput_retained line 212