OAI/Computability/DepthThree/ReversePathEncoding.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.pathRemainder line 22
  2. theorem OAI.DepthThreeLowerBound.pathRemainder_nil line 25
  3. theorem OAI.DepthThreeLowerBound.coveredCount_eq_reverseEligible line 34
  4. def OAI.DepthThreeLowerBound.coveredPathWeight line 50
  5. theorem OAI.DepthThreeLowerBound.coveredPathWeight_nil line 55
  6. theorem OAI.DepthThreeLowerBound.coveredPathWeight_nonneg line 59
  7. theorem OAI.DepthThreeLowerBound.coveredPathWeight_snoc line 63
  8. theorem OAI.DepthThreeLowerBound.remainder_snoc_union_block line 82
  9. theorem OAI.DepthThreeLowerBound.remainder_snoc_disjoint_block line 97
  10. theorem OAI.DepthThreeLowerBound.scope_disjoint_remainder_snoc line 113
  11. def OAI.DepthThreeLowerBound.reverseEncode line 126
  12. theorem OAI.DepthThreeLowerBound.reverseEncode_nil line 131
  13. theorem OAI.DepthThreeLowerBound.reverseEncode_snoc line 140
  14. def OAI.DepthThreeLowerBound.reverseStart line 152
  15. theorem OAI.DepthThreeLowerBound.reverseStart_nil line 155
  16. theorem OAI.DepthThreeLowerBound.reverseStart_cons line 163
  17. theorem OAI.DepthThreeLowerBound.reverseStart_encode line 173
  18. theorem OAI.DepthThreeLowerBound.reverseEncode_indices line 181
  19. def OAI.DepthThreeLowerBound.encodePathPair line 187
  20. theorem OAI.DepthThreeLowerBound.encodePathPair_injective line 191
  21. def OAI.DepthThreeLowerBound.reverseTraces line 204
  22. theorem OAI.DepthThreeLowerBound.mem_reverseTraces_zero line 211
  23. theorem OAI.DepthThreeLowerBound.mem_reverseTraces_succ line 216
  24. theorem OAI.DepthThreeLowerBound.reverseEncode_mem line 224
  25. def OAI.DepthThreeLowerBound.reverseTraceWeight line 247
  26. theorem OAI.DepthThreeLowerBound.reverseTraceWeight_nonneg line 253
  27. theorem OAI.DepthThreeLowerBound.sum_reverseTraces_succ line 262
  28. theorem OAI.DepthThreeLowerBound.sum_reverseTraceWeight line 296
  29. theorem OAI.DepthThreeLowerBound.reverseEncode_weight line 321
  30. def OAI.DepthThreeLowerBound.supportedForwardPairs line 358
  31. def OAI.DepthThreeLowerBound.indexedReverseTraces line 362
  32. theorem OAI.DepthThreeLowerBound.encode_supported_mem line 366
  33. theorem OAI.DepthThreeLowerBound.weighted_supported_paths_le line 373