- Implement algorithm in haskell, split over single steps
  - During presentation show steps working on examples of the problem (one solves during step 1, one fails during step 1, one that requires multiple rotations to be eliminated), within `ghci`
  - For most important proofs (tbd) show applicable step in haskell code with sketch of proof
  
  
# Tables
  - Definition: Tables, embedded tables, embedded pairs, embedded matchings
  - Definition: stable tables
  - Matchings embedded in stable tables are stable (4.2.4 ii)
  - Stable tables are determined by all first OR all last entries (4.2.4 iii)
  - No pair absent from a stable table can block any of it's embedded matchings (4.2.4 i)
  
# Phase 1
  - Removal of pairs from tables
  - Engagement
  - Present algorithm and demonstrate
  - Phase 1 has no effect on the embeddedness of stable pairs (4.2.3 i)
  - Phase 1 stabilizes a table, when it doesn't fail (4.2.2 + 4.2.3 ii)
  - Phase 1 results in the largest stable table (4.2.4 iv)
  
# Rotations
  - Definition: rotation, exposure of rotations in stable tables
  - Directed graphs & tails
  - (Rotations exposed in a stable T are either identical or disjunct (4.2.5))
  
# Phase 2
  - Stable tables that are not already matchings expose at least one rotation and how to find it (4.2.6)
  - Elimination of rotations from stable tables
      - ignores non-elements of rotation (4.2.7 iii)
      - results in table consistent with rotation (4.2.7 i, ii)
      - Thus: produce stable subtables (4.2.8)
  - Subtables that don't agree with an exposed rotation have at least that rotation removed entirely (4.2.9)
      - Any subtable can be created by removing a series of exposed rotations (Cor 4.2.2)
  - Removal of rotations preserve matchings (Thm 4.2.1)
  - Present derived algorithm and demonstrate