Reference · Graph algorithms

rainbow.algorithms.proofs.graph.walk-concat

Graph algorithmssrc/rainbow/algorithms/proofs/graph/walk_concat.clj0 definitions, 5 theorems

CONCATENATING WALKS, for the Floyd-Warshall invariant. A walk x of a arcs ending where a walk y of b arcs starts (x a = y 0) joins into concat x a y = fun t. if t <= a then x t else y (t - a) (b + a arcs) signed/walk-concat : x a = y 0 -> concat 0 = x 0 /\ concat (b + a) = y b /\ walk-length (concat, b + a) ~ walk-length (x, a) + walk-length (y, b) nat/walk-concat-range : x and y within n -> concat within n The length splits with signed/expr-sum-value-append. The first a arcs are x's, and the rest are y's because concat t = y (t - a) from a on (nat/walk-concat-tail, using x a = y 0 at t = a and (i + a) - a = i).

Depends onalgorithms.proofs.graph.walk-cycle-cutmath.nat.monusmath.nat.at-most-cancellation

nat/monus-after-add :
  (i a : ℕ)
  → nat/monus (algebra/nat-add i a) a = i

nat/walk-concat-head :
  (x : ℕ → ℕ) (a : ℕ) (y : ℕ → ℕ) (t : ℕ)
  (ht : t ≤ a)
  → data/Bool.rec (fun x₄ => ℕ) (y (nat/monus t a)) (x t) (nat/decide-at-most t a) = x t

nat/walk-concat-tail :
  (x : ℕ → ℕ) (a : ℕ) (y : ℕ → ℕ)
  (hj : x a = y 0)
  (i : ℕ)
  → data/Bool.rec (fun x₄ => ℕ) (y (nat/monus (algebra/nat-add i a) a)) (x (algebra/nat-add i a)) (most) = y i
  where most := nat/decide-at-most (algebra/nat-add i a) a

signed/walk-concat :
  (W : ℕ → ℕ → ℚ) (x : ℕ → ℕ) (a : ℕ) (y : ℕ → ℕ) (b : ℕ)
  (hj : x a = y 0)
  → proposition/conjunction ((fun t => data/Bool.rec (fun x₁₂ => ℕ) (y (nat/monus t a)) (x t) (nat/decide-at-most t a)) 0 = x 0) (proposition/conjunction ((fun t => data/Bool.rec (fun x₁₈ => ℕ) (y (nat/monus t a)) (x t) (nat/decide-at-most t a)) (algebra/nat-add b a) = y b) (signed/expr-sum-value (fun t => W ((fun t₁ => data/Bool.rec (fun x₂₁ => ℕ) (y (nat/monus t₁ a)) (x t₁) (nat/decide-at-most t₁ a)) t) ((fun t₁ => data/Bool.rec (fun x₂₂ => ℕ) (y (nat/monus t₁ a)) (x t₁) (nat/decide-at-most t₁ a)) (data/succ t))) (algebra/nat-add b a) = value₁ + value))
  where value := signed/expr-sum-value (fun t => W (y t) (y (data/succ t))) b
  where value₁ := signed/expr-sum-value (fun t => W (x t) (x (data/succ t))) a

nat/walk-concat-range :
  (n : ℕ) (x : ℕ → ℕ) (a : ℕ) (y : ℕ → ℕ) (b : ℕ)
  (hj : x a = y 0)
  (hx : ∀ (t : ℕ), ∀ (ht : t ≤ a), nat/strict-below (x t) n)
  (hy : ∀ (t : ℕ), ∀ (ht : t ≤ b), nat/strict-below (y t) n) (t : ℕ)
  (ht : t ≤ algebra/nat-add b a)
  → nat/strict-below ((fun t₁ => data/Bool.rec (fun x₂ => ℕ) (y (nat/monus t₁ a)) (x t₁) (nat/decide-at-most t₁ a)) t) n