OAI/Combinatorics/ThinTrees/BagConstruction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedBag.dense_move line 16
2. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedBag.sparse_move line 76
3. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedBag.interior_move line 168
4. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.ownerEvolution_refl line 244
5. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.ownerEvolution_trans line 248
6. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedBag.interior_loop line 259
7. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.baseToken line 340
8. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrinkRecord line 343
9. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrinkValue line 346
10. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.fresh_base line 350
11. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrink_refines line 357
12. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrink_valid line 365
13. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrink_base line 374
14. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrink_cost line 385
15. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.shrink_discard line 398
16. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.border_shrink_compatible line 411
17. def OAI.StrongThinTree.MultiGraph.Hierarchy.shrinkFamily line 436
18. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.shrinkFamily_valid line 439
19. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.shrinkFamily_sum line 454