OAI/Combinatorics/Chromatic/Walls/TriangularLevelQueues.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.TriangularDynamics.levelQueue line 12
  2. def OAI.ElementaryPositivity.TriangularDynamics.initialLevelQueue line 13
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.mem_levelQueue line 15
  4. lemma OAI.ElementaryPositivity.TriangularDynamics.initialLevelQueue_mem line 17
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.initialLevelQueue_nodup line 28
  6. lemma OAI.ElementaryPositivity.TriangularDynamics.initialLevelQueue_pairwise line 35
  7. lemma OAI.ElementaryPositivity.TriangularDynamics.phaseCycle_levelQueue line 45
  8. lemma OAI.ElementaryPositivity.TriangularDynamics.levelQueue_cons line 54
  9. lemma OAI.ElementaryPositivity.TriangularDynamics.levelQueue_append line 57
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.levelQueue_rotate line 59
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.queue_update_off line 63
  12. def OAI.ElementaryPositivity.ForwardChain.gaps line 79
  13. lemma OAI.ElementaryPositivity.ForwardChain.gaps_append line 83
  14. def OAI.ElementaryPositivity.ForwardChain.positiveMutate line 90
  15. lemma OAI.ElementaryPositivity.ForwardChain.positiveMutate_nonneg line 92
  16. lemma OAI.ElementaryPositivity.ForwardChain.positiveMutate_minus_one line 95
  17. lemma OAI.ElementaryPositivity.ForwardChain.positiveMutate_minus_two line 97
  18. lemma OAI.ElementaryPositivity.ForwardChain.gaps_mutate_last line 102
  19. lemma OAI.ElementaryPositivity.ForwardChain.gaps_mutate_rotation line 117
  20. lemma OAI.ElementaryPositivity.ForwardChain.gaps_rotation_perm line 136
  21. lemma OAI.ElementaryPositivity.ForwardChain.gaps_mutate_fixed line 146