OAI/Combinatorics/HoneycombCorridor/CycleSplice.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.stemGerm line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.reverseLoopGerm line 12
  3. theorem OAI.PolynomialVacuumBridge.Corridor.stem_forward line 14
  4. theorem OAI.PolynomialVacuumBridge.Corridor.stem_reverse line 19
  5. theorem OAI.PolynomialVacuumBridge.Corridor.reverseLoop_advance line 24
  6. theorem OAI.PolynomialVacuumBridge.Corridor.reverseLoop_reverseLoop line 29
  7. theorem OAI.PolynomialVacuumBridge.Corridor.reverseLoop_stem line 34
  8. theorem OAI.PolynomialVacuumBridge.Corridor.reverseGerm_advance_eq line 39
  9. theorem OAI.PolynomialVacuumBridge.Corridor.stem_forward_trace line 43
  10. theorem OAI.PolynomialVacuumBridge.Corridor.stem_forward_terminal line 49
  11. theorem OAI.PolynomialVacuumBridge.Corridor.stem_reverse_trace line 53
  12. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_loop_terminal line 62
  13. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_loop_trace line 70
  14. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_loop_nodup line 79
  15. theorem OAI.PolynomialVacuumBridge.Corridor.dartFlow_reverse line 85
  16. theorem OAI.PolynomialVacuumBridge.Corridor.reverseLoop_outgoing line 89
  17. theorem OAI.PolynomialVacuumBridge.Corridor.wordFlow_reverse line 94
  18. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_loop_flow line 108