OAI/Combinatorics/ThinTrees/Encoding/CanonicalExpansion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Canonical expansion.

  1. def OAI.AlgorithmicThinTrees.BinaryInput.copies line 13
  2. lemma OAI.AlgorithmicThinTrees.BinaryInput.mem_copies line 17
  3. lemma OAI.AlgorithmicThinTrees.BinaryInput.copies_nodup line 22
  4. lemma OAI.AlgorithmicThinTrees.BinaryInput.copies_length line 38
  5. def OAI.AlgorithmicThinTrees.BinaryInput.copiesEquiv line 43
  6. lemma OAI.AlgorithmicThinTrees.BinaryInput.copiesEquiv_apply line 47
  7. def OAI.AlgorithmicThinTrees.BinaryInput.expanded line 50
  8. def OAI.AlgorithmicThinTrees.BinaryInput.labelEquiv line 55
  9. lemma OAI.AlgorithmicThinTrees.BinaryInput.labelEquiv_left line 58
  10. lemma OAI.AlgorithmicThinTrees.BinaryInput.labelEquiv_right line 61
  11. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_cut line 65
  12. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_edgeConnected line 73
  13. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_thinTree line 79
  14. def OAI.AlgorithmicThinTrees.BinaryInput.originalCopy line 89
  15. def OAI.AlgorithmicThinTrees.BinaryInput.originalLabel line 92
  16. lemma OAI.AlgorithmicThinTrees.BinaryInput.originalLabel_eq line 95
  17. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_lift_thinTree line 100
  18. lemma OAI.AlgorithmicThinTrees.BinaryInput.originalCopy_injOn line 107
  19. lemma OAI.AlgorithmicThinTrees.BinaryInput.copies_map line 121
  20. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_lefts line 127
  21. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_rights line 133
  22. lemma OAI.AlgorithmicThinTrees.BinaryInput.expanded_records line 139