CubicPathwidth.Alg.Proofs2.K3Mixed

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T2.TargetBC
import CubicPathwidth.T3.Targets

/-!
# Stage 2 task K3: `algo_mixed` realizes Theorems 2(b), 2(c) and 3 (P, R, S)

Route (tasks K3a–K3c). For `G = ofSimpleGraph S` let `H = (reduceRecord G.copy).1`.
* `H` is well formed, has nodes below `n`, minimum degree `≥ 3` and degrees `≤` those of `G`
  (`ReduceRecordMaximal`, `InducedSpec`).
* `RelabelExists` and `DegreeTransfer` identify `H` with a graph `S'` on `Fin m`,
  `m = H.numNodes ≤ n`, and `S'` has the degree counts of `H` (at most those of `S`).
* `LabelTransfer` turns an injective real labeling `y` of `S'` into rational labels `Y` of
  `H`; `PlainLayoutWidth` bounds the plain sweep of `H` by its largest outer frontier.
* `AlgoMixedWidth` adds `3 log₂ n + 1`; `AlgoMixedNoFallback` gives the flag `false`;
  the Stage 1 theorem `algoMixedExported` gives `HasPathwidthAtMost`.
* If `m` is below the good-labels threshold, any injective labeling is used and the
  width is at most `m`.
-/

noncomputable section
open Classical

namespace CubicPathwidth.Alg

open Graph

namespace K3

/-! ## 1. Graph facts -/

theorem ofS_degree {n : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] (u : Fin n) :
    (Graph.ofSimpleGraph S).degree u.val = S.degree u := by
  unfold Graph.degree
  rw [B2.nbrs_eq, B2.degree_eq_length]

theorem copy_degree_le {G : Graph} (hG : G.WF) (v : Nat) : G.copy.degree v ≤ G.degree v := by
  unfold Graph.degree
  apply List.Subperm.length_le
  apply List.Nodup.subperm ((CubicPathwidth.Alg.T2.copy_wf inducedSpec hG).nbrs_nodup v)
  intro x hx
  exact (CubicPathwidth.Alg.T2.adj_copy_iff inducedSpec hG v x).1 hx

/-- The reduced graph `H` of `algo_mixed`. -/
abbrev redG (G : Graph) : Graph := (reduceRecord G.copy).1

theorem red_facts (hMax : ReduceRecordMaximal) {n : ℕ} (S : SimpleGraph (Fin n))
    [DecidableRel S.Adj] :
    (redG (Graph.ofSimpleGraph S)).WF ∧
      (∀ v ∈ (redG (Graph.ofSimpleGraph S)).nodes, v < n) ∧
      (∀ v ∈ (redG (Graph.ofSimpleGraph S)).nodes, 3 ≤ (redG (Graph.ofSimpleGraph S)).degree v) ∧
      (∀ v ∈ (redG (Graph.ofSimpleGraph S)).nodes,
        (redG (Graph.ofSimpleGraph S)).degree v ≤ (Graph.ofSimpleGraph S).degree v) := by
  obtain ⟨hGw, hGn, -, -⟩ := ofSimpleGraphSpec n S
  have hGc := CubicPathwidth.Alg.T2.copy_wf inducedSpec hGw
  obtain ⟨hHw, hHsub, -, -, -⟩ := reduceRecordSpec _ hGc
  have hM := hMax _ hGc
  refine ⟨hHw, fun v hv => ?_, fun v hv => hM.2.1 v hv, fun v hv => ?_⟩
  · exact (hGn v).1 ((CubicPathwidth.Alg.T2.mem_copy_iff inducedSpec hGw v).1 (hHsub v hv))
  · exact (hM.2.2 v hv).trans (copy_degree_le hGw v)

theorem maxDeg_iff {n k : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj] :
    CubicPathwidth.T2.MaxDegreeAtMost k S ↔ ∀ v, S.degree v ≤ k := by
  unfold CubicPathwidth.T2.MaxDegreeAtMost
  constructor
  · intro h v
    convert h v
  · intro h v
    convert h v

/-! ## 2. The linear bound on `3 log₂ n + 1` -/

theorem log_linear (c η : ℝ) (hc : 0 ≤ c) (hη : 0 < η) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → 3 * (Nat.log 2 n : ℝ) + 1 + c ≤ η * n := by
  have hL : 0 < Real.log 2 := Real.log_pos (by norm_num)
  have hlog : ∀ n : ℕ, 1 ≤ n → (Nat.log 2 n : ℝ) * Real.log 2 ≤ 2 * Real.sqrt n := by
    intro n hn
    have hn0 : (0:ℝ) < n := by exact_mod_cast hn
    have h2 : ((2:ℝ) ^ Nat.log 2 n) ≤ n := by
      exact_mod_cast Nat.pow_log_le_self 2 (by omega)
    have h3 : (Nat.log 2 n : ℝ) * Real.log 2 = Real.log ((2:ℝ) ^ Nat.log 2 n) := by
      rw [Real.log_pow]
    have h4 : Real.log n ≤ 2 * Real.sqrt n := by
      have hs : 0 < Real.sqrt n := Real.sqrt_pos.2 hn0
      have h5 := Real.log_le_sub_one_of_pos hs
      rw [Real.log_sqrt hn0.le] at h5
      linarith
    rw [h3]
    exact (Real.log_le_log (by positivity) h2).trans h4
  set K : ℝ := 6 / Real.log 2 with hK
  have hK0 : 0 ≤ K := by positivity
  set S₀ : ℝ := (K + 1 + c) / η + 1 with hS₀
  have hS₀1 : 1 ≤ S₀ := by
    have : 0 ≤ (K + 1 + c) / η := by positivity
    linarith
  refine ⟨⌈S₀ ^ 2⌉₊ + 1, fun n hn => ?_⟩
  have hn1 : 1 ≤ n := by omega
  have hnS : S₀ ^ 2 ≤ (n : ℝ) := by
    have h : (⌈S₀ ^ 2⌉₊ : ℝ) ≤ n := by
      exact_mod_cast (show ⌈S₀ ^ 2⌉₊ ≤ n by omega)
    exact (Nat.le_ceil _).trans h
  set s : ℝ := Real.sqrt n with hs
  have hs0 : 0 ≤ s := Real.sqrt_nonneg _
  have hsS : S₀ ≤ s := by
    calc S₀ = Real.sqrt (S₀ ^ 2) := (Real.sqrt_sq (by linarith)).symm
      _ ≤ Real.sqrt n := Real.sqrt_le_sqrt hnS
  have hsq : s ^ 2 = (n : ℝ) := Real.sq_sqrt (by positivity)
  have hk : 3 * (Nat.log 2 n : ℝ) ≤ K * s := by
    have h1 : (Nat.log 2 n : ℝ) ≤ 2 * s / Real.log 2 := by
      rw [le_div_iff₀ hL]
      have := hlog n hn1
      linarith
    have h2 : K * s = 6 * s / Real.log 2 := by rw [hK]; ring
    rw [h2]
    calc 3 * (Nat.log 2 n : ℝ) ≤ 3 * (2 * s / Real.log 2) := by linarith
      _ = 6 * s / Real.log 2 := by ring
  have he : η * ((K + 1 + c) / η) = K + 1 + c := by field_simp
  have h1 : K + 1 + c ≤ η * S₀ := by
    have : η * S₀ = η * ((K + 1 + c) / η) + η := by rw [hS₀]; ring
    rw [this, he]
    linarith
  have hA : (K + 1 + c) * s ≤ η * S₀ * s := mul_le_mul_of_nonneg_right h1 hs0
  have hB : η * S₀ * s ≤ η * s * s := by
    apply mul_le_mul_of_nonneg_right _ hs0
    exact mul_le_mul_of_nonneg_left hsS hη.le
  have hC : K * s + 1 + c ≤ (K + 1 + c) * s := by
    nlinarith [mul_nonneg (by linarith : (0:ℝ) ≤ 1 + c) (by linarith : (0:ℝ) ≤ s - 1)]
  calc 3 * (Nat.log 2 n : ℝ) + 1 + c ≤ K * s + 1 + c := by linarith
    _ ≤ η * s * s := by linarith
    _ = η * n := by rw [← hsq]; ring

/-! ## 3. The core: a generic degree-count bound -/

theorem relabel_fin (hX2 : RelabelExists) (H : Graph) (hH : H.WF) :
    ∃ (m : ℕ) (S : SimpleGraph (Fin m)) (e : Fin m → Nat), m = H.numNodes ∧ IsRelabel H S e := by
  obtain ⟨S, e, hIso⟩ := hX2 H hH
  exact ⟨_, S, e, rfl, hIso⟩

theorem mixed_core (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback) (hMax : ReduceRecordMaximal)
    (hX2 : RelabelExists) (hX3 : DegreeTransfer) (hX4 : LabelTransfer) (hPW : PlainLayoutWidth)
    (d : ℕ) (F : ∀ {m : ℕ}, SimpleGraph (Fin m) → ℝ)
    (hF0 : ∀ {m : ℕ} (S : SimpleGraph (Fin m)), 0 ≤ F S)
    (hmono : ∀ {n m : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj]
      (S' : SimpleGraph (Fin m)) (e : Fin m ↪ Fin n),
      CubicPathwidth.T2.MaxDegreeAtMost d S → (∀ i, S'.degree i ≤ S.degree (e i)) → F S' ≤ F S)
    (hgood : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ m : ℕ, N ≤ m → ∀ S' : SimpleGraph (Fin m),
      CubicPathwidth.T2.MinDegreeAtLeast 3 S' → CubicPathwidth.T2.MaxDegreeAtMost d S' →
      ∃ y : Fin m → ℝ, Function.Injective y ∧
        ∀ t : ℝ, ((CubicPathwidth.C3.outerFrontier S' y t).card : ℝ) ≤ F S' + ε * (m : ℝ)) :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ (S : SimpleGraph (Fin n)) [DecidableRel S.Adj],
      CubicPathwidth.T2.MaxDegreeAtMost d S →
      ∃ lab : Labeler, (algoMixedF (Graph.ofSimpleGraph S) lab).2 = false ∧
        HasPathwidthAtMost S (pdWidth (algoMixed (Graph.ofSimpleGraph S) lab)) ∧
        pdWidth (algoMixed (Graph.ofSimpleGraph S) lab) ≤ F S + ε * (n : ℝ) := by
  classical
  intro ε hε
  obtain ⟨N₁, hN₁⟩ := hgood (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ := log_linear (N₁ : ℝ) (ε / 2) (by positivity) (by linarith)
  refine ⟨N₂, fun n hn S _ hS => ?_⟩
  have hn' := hN₂ n hn
  have hS' : ∀ v, S.degree v ≤ d := (maxDeg_iff S).1 hS
  obtain ⟨hHw, hHn, hHmin, hHmax⟩ := red_facts hMax S
  obtain ⟨hGw, hGn, -, -⟩ := ofSimpleGraphSpec n S
  obtain ⟨m, S', e, hm, hIso⟩ := relabel_fin hX2 _ hHw
  have hinj : Function.Injective e := hIso.1
  have hnodes := hIso.2.1
  have hdeg : ∀ i, S'.degree i = (redG (Graph.ofSimpleGraph S)).degree (e i) :=
    hX3 _ m S' e hHw hIso
  have hemem : ∀ i, e i ∈ (redG (Graph.ofSimpleGraph S)).nodes :=
    fun i => (hnodes (e i)).2 ⟨i, rfl⟩
  have helt : ∀ i, e i < n := fun i => hHn _ (hemem i)
  let e' : Fin m ↪ Fin n :=
    ⟨fun i => ⟨e i, helt i⟩, fun i j h => hinj (congrArg Fin.val h)⟩
  have hGS : ∀ i, (redG (Graph.ofSimpleGraph S)).degree (e i) ≤ S.degree (e' i) := fun i => by
    have h1 := hHmax _ (hemem i)
    have h2 : (Graph.ofSimpleGraph S).degree (e i) = S.degree (e' i) := ofS_degree S (e' i)
    omega
  have hSdeg : ∀ i, S'.degree i ≤ S.degree (e' i) := fun i => by
    rw [hdeg i]
    exact hGS i
  have hmin : CubicPathwidth.T2.MinDegreeAtLeast 3 S' := by
    intro i
    rw [hdeg i]
    exact hHmin _ (hemem i)
  have hmaxS' : CubicPathwidth.T2.MaxDegreeAtMost d S' := by
    intro i
    rw [hdeg i]
    exact (hGS i).trans (hS' _)
  have hmn : m ≤ n := by
    have := Fintype.card_le_of_injective e' e'.injective
    simpa using this
  have hmn' : (m : ℝ) ≤ n := by exact_mod_cast hmn
  have hF := hmono S S' e' hS hSdeg
  have hF0S := hF0 S
  -- labels of `H`
  have hY : ∃ Y : Labels, LabelsInjOn (redG (Graph.ofSimpleGraph S)) Y ∧ ∃ W : ℝ,
      (∀ t : ℚ, ((outerFr (redG (Graph.ofSimpleGraph S)) Y t).length : ℝ) ≤ W) ∧
        W + 3 * (Nat.log 2 n : ℝ) + 1 ≤ F S + ε * (n : ℝ) := by
    by_cases hmN : N₁ ≤ m
    · obtain ⟨y, hyinj, hyfr⟩ := hN₁ m hmN S' hmin hmaxS'
      obtain ⟨Y, hYinj, -, hYout, -, -⟩ := hX4 _ m S' e hHw hIso y hyinj
      refine ⟨Y, hYinj, F S' + ε / 2 * (m : ℝ), fun t => ?_, ?_⟩
      · obtain ⟨s, -, hs⟩ := hYout t
        rw [hs]
        exact hyfr s
      · have h1 : ε / 2 * (m : ℝ) ≤ ε / 2 * n := mul_le_mul_of_nonneg_left hmn' (by positivity)
        have h2 : (0 : ℝ) ≤ N₁ := by positivity
        linarith
    · have hmN0 : m < N₁ := not_le.1 hmN
      have hy0 : Function.Injective (fun i : Fin m => ((i : ℕ) : ℝ)) := by
        intro i j h
        have h' : ((i : ℕ) : ℝ) = ((j : ℕ) : ℝ) := h
        exact Fin.ext (by exact_mod_cast h')
      obtain ⟨Y, hYinj, -, -, -, -⟩ := hX4 _ m S' e hHw hIso _ hy0
      refine ⟨Y, hYinj, (m : ℝ), fun t => ?_, ?_⟩
      · have h1 : (outerFr (redG (Graph.ofSimpleGraph S)) Y t).length ≤ m := by
          rw [hm]
          exact List.length_filter_le _ _
        exact_mod_cast h1
      · have hmN' : (m : ℝ) ≤ N₁ := by exact_mod_cast hmN0.le
        have h1 : (0 : ℝ) ≤ ε * n := by positivity
        linarith
  obtain ⟨Y, hYinj, W, hWout, hWb⟩ := hY
  let lab : Labeler := fun G' => if G' = redG (Graph.ofSimpleGraph S) then Y else fun _ => 0
  have hlab : lab (redG (Graph.ofSimpleGraph S)) = Y := by simp [lab]
  have hflag : (algoMixedF (Graph.ofSimpleGraph S) lab).2 = false := hN _ hGw lab
  have hwid : pdWidth (algoMixed (Graph.ofSimpleGraph S) lab) ≤
      pdWidth (plainLayout (redG (Graph.ofSimpleGraph S)) (lab (redG (Graph.ofSimpleGraph S)))) +
        3 * (Nat.log 2 (Graph.ofSimpleGraph S).numNodes : ℝ) + 1 := hW _ hGw lab hflag
  have hnum : (Graph.ofSimpleGraph S).numNodes = n := by
    unfold Graph.numNodes
    rw [B2.nodes_eq, List.length_range]
  rw [hlab, hnum] at hwid
  have hpl : pdWidth (plainLayout (redG (Graph.ofSimpleGraph S)) Y) ≤ W :=
    hPW _ hHw Y hYinj W hWout
  refine ⟨lab, hflag, algoMixedExported n S lab, ?_⟩
  linarith

/-! ## 4. Degree-count instances (`MixedRealizes4`, `MixedRealizes5`) -/

theorem mixedRealizes4_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) (a₃ a₄ : ℝ) (h0 : 0 ≤ a₃) (h34 : a₃ ≤ a₄)
    (hgood : CubicPathwidth.T2.GoodLabelsCount a₃ a₄) : MixedRealizes4 a₃ a₄ :=
  mixed_core hW hN hMax hX2 hX3 hX4 hPW 4
    (fun {_} S => a₃ * (CubicPathwidth.T2.degreeCount S 3 : ℝ) +
      a₄ * (CubicPathwidth.T2.degreeCount S 4 : ℝ))
    (fun {_} S => add_nonneg (mul_nonneg h0 (Nat.cast_nonneg _))
      (mul_nonneg (h0.trans h34) (Nat.cast_nonneg _)))
    (fun {_ _} S _ S' e hS hdeg =>
      CubicPathwidth.T2.degreeCount_transfer S S' e (fun i => by convert hdeg i) hS h0 h34)
    hgood

theorem mixedRealizes5_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) (a₃ a₄ a₅ : ℝ) (h0 : 0 ≤ a₃) (h34 : a₃ ≤ a₄)
    (h45 : a₄ ≤ a₅) (hgood : CubicPathwidth.T3.GoodLabelsCount5 a₃ a₄ a₅) :
    MixedRealizes5 a₃ a₄ a₅ :=
  mixed_core hW hN hMax hX2 hX3 hX4 hPW 5
    (fun {_} S => a₃ * (CubicPathwidth.T2.degreeCount S 3 : ℝ) +
      a₄ * (CubicPathwidth.T2.degreeCount S 4 : ℝ) +
      a₅ * (CubicPathwidth.T2.degreeCount S 5 : ℝ))
    (fun {_} S => add_nonneg (add_nonneg (mul_nonneg h0 (Nat.cast_nonneg _))
      (mul_nonneg (h0.trans h34) (Nat.cast_nonneg _)))
      (mul_nonneg ((h0.trans h34).trans h45) (Nat.cast_nonneg _)))
    (fun {_ _} S _ S' e hS hdeg =>
      CubicPathwidth.T3.degreeCount_transfer5 S S' e (fun i => by convert hdeg i) hS h0 h34 h45)
    hgood

end K3

/-! ## 5. The five main statements -/

open K3

theorem algoMixedRealizesTheorem2b_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) : AlgoMixedRealizesTheorem2b := fun hadm =>
  mixedRealizes4_of hW hN hMax hX2 hX3 hX4 hPW CubicPathwidth.T2.Fcubic (103 / 400)
    (by linarith [CubicPathwidth.T2.Fcubic_ge]) CubicPathwidth.T2.Fcubic_le
    (CubicPathwidth.T2.goodLabelsCount_of CubicPathwidth.T2.degreeLabels_cut
      CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T2.charging hadm
      (CubicPathwidth.T2.four_Phi_neg_three_le.trans CubicPathwidth.T2.Fcubic_ge)
      CubicPathwidth.T2.Fcubic_le)

theorem algoMixedRealizesTheorem2c_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) : AlgoMixedRealizesTheorem2c := fun hadm =>
  mixedRealizes4_of hW hN hMax hX2 hX3 hX4 hPW (5 / 32) (1 / 4) (by norm_num) (by norm_num)
    (CubicPathwidth.T2.goodLabelsCount_of CubicPathwidth.T2.degreeLabels_cut
      CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T2.charging hadm
      (CubicPathwidth.T2.four_Phi_neg_three_le.trans (by norm_num)) (by norm_num))

theorem algoMixedRealizesTheorem3P_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) : AlgoMixedRealizesTheorem3P := fun hadm =>
  mixedRealizes5_of hW hN hMax hX2 hX3 hX4 hPW CubicPathwidth.T2.Fcubic (103 / 400)
    (3667 / 10000) (by linarith [CubicPathwidth.T2.Fcubic_ge])
    CubicPathwidth.T3.triple_P_mono.1 CubicPathwidth.T3.triple_P_mono.2
    (CubicPathwidth.T3.goodLabelsCount5_step CubicPathwidth.T3.degreeLabels5
      CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T3.charging5
      CubicPathwidth.T2.Fcubic (103 / 400) (3667 / 10000) hadm CubicPathwidth.T3.tail_P
      CubicPathwidth.T3.triple_P_mono.1 CubicPathwidth.T3.triple_P_mono.2)

theorem algoMixedRealizesTheorem3R_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) : AlgoMixedRealizesTheorem3R := fun hadm =>
  mixedRealizes5_of hW hN hMax hX2 hX3 hX4 hPW (291 / 2000) (253 / 1000) (9 / 25)
    (by norm_num) (by norm_num) (by norm_num)
    (CubicPathwidth.T3.goodLabelsCount5_step CubicPathwidth.T3.degreeLabels5
      CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T3.charging5
      (291 / 2000) (253 / 1000) (9 / 25) hadm CubicPathwidth.T3.tail_R (by norm_num)
      (by norm_num))

theorem algoMixedRealizesTheorem3S_of (hW : AlgoMixedWidth) (hN : AlgoMixedNoFallback)
    (hMax : ReduceRecordMaximal) (hX2 : RelabelExists) (hX3 : DegreeTransfer)
    (hX4 : LabelTransfer) (hPW : PlainLayoutWidth) : AlgoMixedRealizesTheorem3S := fun hadm =>
  mixedRealizes5_of hW hN hMax hX2 hX3 hX4 hPW (5 / 32) (1 / 4) (11 / 32)
    (by norm_num) (by norm_num) (by norm_num)
    (CubicPathwidth.T3.goodLabelsCount5_step CubicPathwidth.T3.degreeLabels5
      CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T3.charging5
      (5 / 32) (1 / 4) (11 / 32) hadm CubicPathwidth.T3.tail_S (by norm_num) (by norm_num))

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2b_of
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem2c_of
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3P_of
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3R_of
#print axioms CubicPathwidth.Alg.algoMixedRealizesTheorem3S_of