OAI/Computability/DepthThree/SparseBranch.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.sparseBatchUpdate line 14
  2. theorem OAI.DepthThreeLowerBound.mem_sparseBatchUpdate line 18
  3. theorem OAI.DepthThreeLowerBound.batch_subset_sparseBatchUpdate line 23
  4. theorem OAI.DepthThreeLowerBound.sparseBatchUpdate_subset_union line 26
  5. theorem OAI.DepthThreeLowerBound.sparseBatchUpdate_mono_left line 34
  6. theorem OAI.DepthThreeLowerBound.sparseBatchUpdate_dominates line 41
  7. theorem OAI.DepthThreeLowerBound.sparseBatchUpdate_satisfies line 49
  8. theorem OAI.DepthThreeLowerBound.bool_eq_of_true_iff line 64

    Also declared: OAI/Computability/DepthThree/SparseNormalize.lean:39 (same declaration text).

  9. structure OAI.DepthThreeLowerBound.SparseState line 67
  10. def OAI.DepthThreeLowerBound.SparseState.toCNF line 74
  11. def OAI.DepthThreeLowerBound.SparseState.eval line 77
  12. structure OAI.DepthThreeLowerBound.SparseState.Valid line 79
  13. theorem OAI.DepthThreeLowerBound.SparseState.eval_eq_true line 86
  14. def OAI.DepthThreeLowerBound.SparseState.batchUpdate line 110
  15. theorem OAI.DepthThreeLowerBound.SparseState.batchUpdate_active line 115
  16. theorem OAI.DepthThreeLowerBound.SparseState.batchUpdate_side line 118
  17. theorem OAI.DepthThreeLowerBound.SparseState.batchUpdate_added line 121
  18. theorem OAI.DepthThreeLowerBound.SparseState.eval_batchUpdate_eq_true line 124
  19. structure OAI.DepthThreeLowerBound.InsertionBatch line 139
  20. theorem OAI.DepthThreeLowerBound.InsertionBatch.clause_nonempty line 153
  21. theorem OAI.DepthThreeLowerBound.InsertionBatch.antichain line 162
  22. theorem OAI.DepthThreeLowerBound.InsertionBatch.fresh line 170
  23. theorem OAI.DepthThreeLowerBound.InsertionBatch.not_mem_active line 184
  24. theorem OAI.DepthThreeLowerBound.InsertionBatch.disjoint_active line 188
  25. theorem OAI.DepthThreeLowerBound.InsertionBatch.disjoint_added line 193
  26. theorem OAI.DepthThreeLowerBound.InsertionBatch.removed_strict line 199
  27. theorem OAI.DepthThreeLowerBound.InsertionBatch.normalized line 210
  28. theorem OAI.DepthThreeLowerBound.InsertionBatch.width_le line 221
  29. theorem OAI.DepthThreeLowerBound.InsertionBatch.valid_batchUpdate line 232
  30. theorem OAI.DepthThreeLowerBound.InsertionBatch.literal_occurrences_le_one line 257
  31. theorem OAI.DepthThreeLowerBound.InsertionBatch.added_eq line 269
  32. structure OAI.DepthThreeLowerBound.SignedSunflower line 276
  33. theorem OAI.DepthThreeLowerBound.SignedSunflower.card_family_ge_two line 290
  34. theorem OAI.DepthThreeLowerBound.SignedSunflower.family_nonempty line 294
  35. theorem OAI.DepthThreeLowerBound.SignedSunflower.size_ge_two line 297
  36. theorem OAI.DepthThreeLowerBound.SignedSunflower.size_le line 302
  37. def OAI.DepthThreeLowerBound.SignedSunflower.petals line 307
  38. theorem OAI.DepthThreeLowerBound.SignedSunflower.mem_petals line 310
  39. def OAI.DepthThreeLowerBound.SignedSunflower.coreBatch line 313
  40. def OAI.DepthThreeLowerBound.SignedSunflower.petalBatch line 335
  41. def OAI.DepthThreeLowerBound.SignedSunflower.batch line 367
  42. def OAI.DepthThreeLowerBound.SignedSunflower.coreBranch line 370
  43. def OAI.DepthThreeLowerBound.SignedSunflower.petalBranch line 373
  44. def OAI.DepthThreeLowerBound.SignedSunflower.branch line 376
  45. theorem OAI.DepthThreeLowerBound.SignedSunflower.branch_active line 379
  46. theorem OAI.DepthThreeLowerBound.SignedSunflower.branch_added line 383
  47. theorem OAI.DepthThreeLowerBound.SignedSunflower.batch_card line 387
  48. theorem OAI.DepthThreeLowerBound.SignedSunflower.coreBranch_valid line 393
  49. theorem OAI.DepthThreeLowerBound.SignedSunflower.petalBranch_valid line 396
  50. theorem OAI.DepthThreeLowerBound.SignedSunflower.branch_valid line 401
  51. theorem OAI.DepthThreeLowerBound.SignedSunflower.core_false_iff_complement_units line 407
  52. theorem OAI.DepthThreeLowerBound.SignedSunflower.petals_true_of_core_false line 428
  53. theorem OAI.DepthThreeLowerBound.SignedSunflower.eval_coreBranch line 441
  54. theorem OAI.DepthThreeLowerBound.SignedSunflower.eval_petalBranch line 448
  55. theorem OAI.DepthThreeLowerBound.SignedSunflower.branch_indicator line 471
  56. theorem OAI.DepthThreeLowerBound.SignedSunflower.branch_disjoint line 477