CubicPathwidth.Alg.Proofs2.A1TopWidth

Source file CubicPathwidth/Alg/Proofs2/A1TopWidth.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2

/-!
Stage 2 task A1: `AlgoT1Width` from `SwitchedLayoutWidth`, and `AlgoT2aWidth` from
`PlainLayoutWidth`. `algoT1 G Y = switchedLayout G Y` and `algoT2a G Y = plainLayout G Y`
by unfolding the definitions of `Port.lean`.
-/

namespace CubicPathwidth.Alg

open Graph

/-- Theorem 1 algorithm: the width bound follows from the switched-layout bridge. -/
theorem algoT1Width_of (h : SwitchedLayoutWidth) : AlgoT1Width := by
  unfold AlgoT1Width
  intro G hG hdeg Y hinj hnz w h1 h2 h3
  exact (h G hG hdeg Y hinj hnz w h1 h2 h3).2

/-- Theorem 2(a) algorithm: the width bound follows from the plain-layout bridge. -/
theorem algoT2aWidth_of (h : PlainLayoutWidth) : AlgoT2aWidth := by
  unfold AlgoT2aWidth
  intro G hG Y hinj w h1
  exact h G hG Y hinj w h1

#print axioms CubicPathwidth.Alg.algoT1Width_of
#print axioms CubicPathwidth.Alg.algoT2aWidth_of

end CubicPathwidth.Alg
Back to top