@[reducible, inline]

abbrev Chapter9.Vertex : Type

Equations

• Chapter9.Vertex = ℕ

@[reducible, inline]

abbrev Chapter9.Weight : Type

Equations

• Chapter9.Weight = ℤ

@[reducible, inline]

abbrev Chapter9.Edge : Type

Equations

• Chapter9.Edge = (Chapter9.Vertex × Chapter9.Vertex × Chapter9.Weight)

@[reducible, inline]

abbrev Chapter9.Graph : Type

Equations

• Chapter9.Graph = (List Chapter9.Vertex × List Chapter9.Edge)

def Chapter9.nodes (g : Graph) : List Vertex

Equations

• Chapter9.nodes g = g.1

def Chapter9.edges (g : Graph) : List Edge

Equations

• Chapter9.edges g = g.2

def Chapter9.souce (e : Edge) : Vertex

Equations

• Chapter9.souce e = e.1

def Chapter9.target (e : Edge) : Vertex

Equations

• Chapter9.target e = e.2.1

def Chapter9.weight (e : Edge) : Weight

Equations

• Chapter9.weight e = e.2.2

@[reducible, inline]

abbrev Chapter9.AdjArray : Type

Equations

• Chapter9.AdjArray = Lean.AssocList Chapter9.Vertex (List (Chapter9.Vertex × Chapter9.Weight))

@[reducible, inline]

abbrev Chapter9.Tree : Type

Equations

• Chapter9.Tree = Chapter9.Graph

@[reducible, inline]

abbrev Chapter9.Forest : Type

Equations

• Chapter9.Forest = List Chapter9.Tree

def Chapter9.cost (t : Tree) : ℤ

Equations

• Chapter9.cost t = (List.map Chapter9.weight (Chapter9.edges t)).sum

@[reducible, inline]

abbrev Chapter9.SpanningTrees.State : Type

Equations

• Chapter9.SpanningTrees.State = (Chapter9.Forest × List Chapter9.Edge)

def Chapter9.SpanningTrees.extract (s : State) : Tree

Equations

• Chapter9.SpanningTrees.extract s = List.head! s.1

def Chapter9.SpanningTrees.done (s : State) : Bool

Equations

• Chapter9.SpanningTrees.done s = decide (List.length s.1 = 1)

def Chapter9.SpanningTrees.start₀ (g : Graph) : State

Equations

• Chapter9.SpanningTrees.start₀ g = (List.map (fun (v : Chapter9.Vertex) => ([v], [])) (Chapter9.nodes g), Chapter9.edges g)

def Chapter9.SpanningTrees.find (ts : Forest) (v : Vertex) : Tree

Equations

• Chapter9.SpanningTrees.find ts v = (List.find? (fun (t : Chapter9.Graph) => (Chapter9.nodes t).contains v) ts).get!

def Chapter9.SpanningTrees.safeEdge (e : Edge) (ts : Forest) : Bool

Equations

• Chapter9.SpanningTrees.safeEdge e ts = decide (Chapter9.SpanningTrees.find ts (Chapter9.souce e) ≠ Chapter9.SpanningTrees.find ts (Chapter9.target e))

def Chapter9.SpanningTrees.add (e : Edge) (ts : Forest) : Forest

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.SpanningTrees.steps : State → List State

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.SpanningTrees.spats (g : Graph) : List Tree

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.SpanningTrees.MCC (g : Graph) : Tree

Equations

• Chapter9.SpanningTrees.MCC g = Chapter7.minWith Chapter9.cost (Chapter9.SpanningTrees.spats g)

@[irreducible]

def Chapter9.SpanningTrees.gstep (s : State) : State

Equations

• One or more equations did not get rendered due to their size.
• Chapter9.SpanningTrees.gstep (fst, []) = (fst, [])

def Chapter9.SpanningTrees.start₁ (g : Graph) : State

Equations

• Chapter9.SpanningTrees.start₁ g = (List.map (fun (v : Chapter9.Vertex) => ([v], [])) (Chapter9.nodes g), Chapter5.sortOn₃ Chapter9.weight (Chapter9.edges g))

def Chapter9.SpanningTrees.kruskal₁ (g : Graph) : Tree

Equations

• Chapter9.SpanningTrees.kruskal₁ g = Chapter9.SpanningTrees.extract (Chapter1.until' Chapter9.SpanningTrees.done Chapter9.SpanningTrees.gstep (Chapter9.SpanningTrees.start₁ g))

def Chapter9.SpanningTrees.kruskal₂ (g : Graph) : Tree

Equations

• Chapter9.SpanningTrees.kruskal₂ g = Chapter9.SpanningTrees.extract (Chapter1.apply ((Chapter9.nodes g).length - 1) Chapter9.SpanningTrees.gstep (Chapter9.SpanningTrees.start₁ g))

@[reducible, inline]

abbrev Chapter9.primsalgorithm.State : Type

Equations

• Chapter9.primsalgorithm.State = (Chapter9.Tree × List Chapter9.Edge)

def Chapter9.primsalgorithm.add (e : Edge) (t : Tree) : Tree

Equations

• Chapter9.primsalgorithm.add e (vs, es) = bif vs.contains (Chapter9.souce e) then (Chapter9.target e :: vs, e :: es) else (Chapter9.souce e :: vs, e :: es)

def Chapter9.primsalgorithm.safeEdge (e : Edge) (t : Tree) : Bool

Equations

• Chapter9.primsalgorithm.safeEdge e t = decide ((Chapter9.nodes t).contains (Chapter9.souce e) ≠ (Chapter9.nodes t).contains (Chapter9.target e))

def Chapter9.primsalgorithm.steps (s : State) : List State

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.primsalgorithm.spats (g : Graph) : List Tree

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Chapter9.primsalgorithm.spats.helper (done : State → Bool) (ss : List State) (fuel : ℕ) : List Tree

Equations

• One or more equations did not get rendered due to their size.
• Chapter9.primsalgorithm.spats.helper done ss 0 = panicWithPosWithDecl "Fad.Chapter9" "Chapter9.primsalgorithm.spats.helper" 139 20 "Never here"

def Chapter9.primsalgorithm.mcst : Graph → Tree

Equations

• Chapter9.primsalgorithm.mcst = Chapter7.minWith Chapter9.cost ∘ Chapter9.primsalgorithm.spats

@[irreducible]

def Chapter9.primsalgorithm.gstep : State → State

Equations

• One or more equations did not get rendered due to their size.
• Chapter9.primsalgorithm.gstep (t, []) = (t, [])

def Chapter9.primsalgorithm.prim (g : Graph) : Tree

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Chapter9.primsalgorithm.prim.helper (done : State → Bool) (s : State) (fuel : ℕ) : State

Equations

• Chapter9.primsalgorithm.prim.helper done s 0 = panicWithPosWithDecl "Fad.Chapter9" "Chapter9.primsalgorithm.prim.helper" 172 18 "Never Here"
• Chapter9.primsalgorithm.prim.helper done s fuel_2.succ = bif done s then s else Chapter9.primsalgorithm.prim.helper done (Chapter9.primsalgorithm.gstep s) fuel_2

def Chapter9.primsalgorithm.prim' (g : Graph) : Tree

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Chapter9.primsalgorithm.Links : Type

Equations

• Chapter9.primsalgorithm.Links = Std.HashMap Chapter9.Vertex (Chapter9.Vertex × Chapter9.Weight)

@[reducible, inline]

abbrev Chapter9.primsalgorithm.State' : Type

Equations

• Chapter9.primsalgorithm.State' = (Chapter9.primsalgorithm.Links × List Chapter9.Vertex)

def Chapter9.primsalgorithm.parent (ls : Links) (v : Vertex) : Vertex

Equations

• Chapter9.primsalgorithm.parent ls v = (Std.HashMap.get! ls v).1

def Chapter9.primsalgorithm.weight' (ls : Links) (v : Vertex) : Weight

Equations

• Chapter9.primsalgorithm.weight' ls v = (Std.HashMap.get! ls v).2

@[reducible, inline]

abbrev Chapter9.primsalgorithm.Weights : Type

Equations

• Chapter9.primsalgorithm.Weights = Std.HashMap (Chapter9.Vertex × Chapter9.Vertex) Chapter9.Weight

def Chapter9.primsalgorithm.start (n : ℕ) : State'

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.primsalgorithm.gstep' (wa : Weights) (s : State') : State'

Equations

• One or more equations did not get rendered due to their size.

def Chapter9.primsalgorithm.extract (s : State') : Tree

Equations

• One or more equations did not get rendered due to their size.