inductive Chapter8.S1.Tree (α : Type) : Type

• leaf {α : Type} : α → Tree α
• node {α : Type} : Tree α → Tree α → Tree α

def Chapter8.S1.instReprTree.repr {α✝ : Type} [Repr α✝] : Tree α✝ → ℕ → Std.Format

Equations

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

instance Chapter8.S1.instReprTree {α✝ : Type} [Repr α✝] : Repr (Tree α✝)

Equations

• Chapter8.S1.instReprTree = { reprPrec := Chapter8.S1.instReprTree.repr }

def Chapter8.S1.instInhabitedTree.default {a✝ : Type} [Inhabited a✝] : Tree a✝

Equations

• Chapter8.S1.instInhabitedTree.default = Chapter8.S1.Tree.leaf default

instance Chapter8.S1.instInhabitedTree {a✝ : Type} [Inhabited a✝] : Inhabited (Tree a✝)

Equations

• Chapter8.S1.instInhabitedTree = { default := Chapter8.S1.instInhabitedTree.default }

def Chapter8.S1.Tree.size {α : Type} : Tree α → ℕ

Equations

• (Chapter8.S1.Tree.leaf a).size = 1
• (a.node a_1).size = a.size + a_1.size

def Chapter8.S1.Tree.height {α : Type} : Tree α → ℕ

Equations

• (Chapter8.S1.Tree.leaf a).height = 0
• (a.node a_1).height = a.height.max a_1.height + 1

def Chapter8.S1.Tree.fringe {α : Type} : Tree α → List α

Equations

• (Chapter8.S1.Tree.leaf a).fringe = [a]
• (a.node a_1).fringe = a.fringe ++ a_1.fringe

@[irreducible]

def Chapter8.S1.mkTree {a : Type} [Inhabited a] (as : List a) : Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter8.S1.mkTree [] = Chapter8.S1.Tree.leaf default

def Chapter8.S1.mkTree₁ {a : Type} [Inhabited a] : List a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter8.S1.mkTree₁ [] = Chapter8.S1.Tree.leaf default

def Chapter8.S1.cost : Tree ℕ → ℕ

Equations

• Chapter8.S1.cost (Chapter8.S1.Tree.leaf x_1) = x_1
• Chapter8.S1.cost (t₁.node t₂) = 1 + (Chapter8.S1.cost t₁).max (Chapter8.S1.cost t₂)

def Chapter8.S1.extend {a : Type} (x : a) : Tree a → List (Tree a)

Equations

• Chapter8.S1.extend x (Chapter8.S1.Tree.leaf a_1) = [(Chapter8.S1.Tree.leaf x).node (Chapter8.S1.Tree.leaf a_1)]
• Chapter8.S1.extend x (a_1.node a_2) = [(Chapter8.S1.Tree.leaf x).node (a_1.node a_2)] ++ List.map (fun (x : Chapter8.S1.Tree a) => x.node a_2) (Chapter8.S1.extend x a_1)

def Chapter8.S1.mkTrees {a : Type} [Inhabited a] : List a → List (Tree a)

Equations

• Chapter8.S1.mkTrees [] = []
• Chapter8.S1.mkTrees [x_1] = [Chapter8.S1.Tree.leaf x_1]
• Chapter8.S1.mkTrees (x_1 :: xs) = Chapter1.concatMap (Chapter8.S1.extend x_1) (Chapter8.S1.mkTrees xs)

def Chapter8.S1.foldrn {α β : Type} [Inhabited β] (f : α → β → β) (g : α → β) : List α → β

Equations

• Chapter8.S1.foldrn f g [] = default
• Chapter8.S1.foldrn f g [x_1] = g x_1
• Chapter8.S1.foldrn f g (x_1 :: xs) = f x_1 (Chapter8.S1.foldrn f g xs)

def Chapter8.S1.mkTrees₁ {a : Type} [Inhabited a] : List a → List (Tree a)

Equations

• Chapter8.S1.mkTrees₁ = Chapter8.S1.foldrn (Chapter1.concatMap ∘ Chapter8.S1.extend) (Chapter1.wrap ∘ Chapter8.S1.Tree.leaf)

@[reducible, inline]

abbrev Chapter8.S1.Forest (a : Type) : Type

Equations

• Chapter8.S1.Forest a = List (Chapter8.S1.Tree a)

def Chapter8.S1.rollup {a : Type} [Inhabited (Tree a)] : List (Tree a) → Tree a

Equations

• Chapter8.S1.rollup = Chapter6.foldl1 Chapter8.S1.Tree.node

def Chapter8.S1.spine {a : Type} : Tree a → List (Tree a)

Equations

• Chapter8.S1.spine (Chapter8.S1.Tree.leaf a_1) = [Chapter8.S1.Tree.leaf a_1]
• Chapter8.S1.spine (a_1.node a_2) = Chapter8.S1.spine a_1 ++ [a_2]

def Chapter8.S1.extend₁ {a : Type} [Inhabited a] (x : a) (ts : Forest a) : List (Forest a)

Equations

• Chapter8.S1.extend₁ x ts = List.map (fun (i : ℕ) => Chapter8.S1.Tree.leaf x :: Chapter8.S1.rollup (List.take i ts) :: List.drop i ts) (List.range' 1 (List.length ts))

def Chapter8.S1.mkForests {a : Type} [Inhabited a] : List a → List (Forest a)

Equations

• Chapter8.S1.mkForests = Chapter8.S1.foldrn (Chapter1.concatMap ∘ Chapter8.S1.extend₁) (Chapter1.wrap ∘ Chapter1.wrap ∘ Chapter8.S1.Tree.leaf)

def Chapter8.S1.mkTrees₂ {a : Type} [Inhabited a] : List a → List (Tree a)

Equations

• Chapter8.S1.mkTrees₂ = List.map Chapter8.S1.rollup ∘ Chapter8.S1.mkForests

def Chapter8.S1.mct₀ : List ℕ → Tree ℕ

Equations

• Chapter8.S1.mct₀ = Chapter7.minWith Chapter8.S1.cost ∘ Chapter8.S1.mkTrees₂

def Chapter8.S1.scanl1 {a : Type u_1} (f : a → a → a) : List a → List a

Equations

• Chapter8.S1.scanl1 f (x_1 :: xs) = Chapter1.scanl f x_1 xs
• Chapter8.S1.scanl1 f [] = []

def Chapter8.S1.lcost : Tree ℕ → List ℕ

Equations

• Chapter8.S1.lcost = List.reverse ∘ (Chapter8.S1.scanl1 fun (x y : ℕ) => 1 + x.max y) ∘ List.map Chapter8.S1.cost ∘ Chapter8.S1.spine

def Chapter8.S1.add (x : ℕ) (ts : List (Tree ℕ)) : List (Tree ℕ)

Equations

• Chapter8.S1.add x ts = Chapter8.S1.Tree.leaf x :: Chapter8.S1.add.join x ts

@[irreducible]

def Chapter8.S1.add.join (x : ℕ) : List (Tree ℕ) → List (Tree ℕ)

Equations

• Chapter8.S1.add.join x [u] = [u]
• Chapter8.S1.add.join x [] = []
• Chapter8.S1.add.join x (u :: v :: ts) = if x.max (Chapter8.S1.cost u) < Chapter8.S1.cost v then u :: v :: ts else Chapter8.S1.add.join x (u.node v :: ts)

def Chapter8.S1.mct₁ : List ℕ → Tree ℕ

Equations

• Chapter8.S1.mct₁ = Chapter8.S1.foldrn (fun (x : ℕ) => Chapter8.S1.rollup ∘ Chapter8.S1.add x ∘ Chapter8.S1.spine) Chapter8.S1.Tree.leaf

@[reducible, inline]

abbrev Chapter8.S1.Pair : Type

Equations

• Chapter8.S1.Pair = (Chapter8.S1.Tree ℕ × ℕ)

def Chapter8.S1.node : Pair → Pair → Pair

Equations

• Chapter8.S1.node (u, c) (v, d) = (u.node v, 1 + c.max d)

def Chapter8.S1.leaf : ℕ → Pair

Equations

• Chapter8.S1.leaf x✝ = (Chapter8.S1.Tree.leaf x✝, x✝)

@[irreducible]

def Chapter8.S1.join (x : ℕ) : List Pair → List Pair

Equations

• Chapter8.S1.join x [u] = [u]
• Chapter8.S1.join x [] = []
• Chapter8.S1.join x (u :: v :: ts) = if x.max u.2 < v.2 then u :: v :: ts else Chapter8.S1.join x (Chapter8.S1.node u v :: ts)

def Chapter8.S1.mct : List ℕ → Tree ℕ

Equations

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

def Chapter8.S2.depths {a : Type} : S1.Tree a → List ℕ

Equations

• Chapter8.S2.depths = Chapter8.S2.depths.frm 0

def Chapter8.S2.depths.frm {a : Type} (n : ℕ) : S1.Tree a → List ℕ

Equations

• Chapter8.S2.depths.frm n (Chapter8.S1.Tree.leaf a_1) = [n]
• Chapter8.S2.depths.frm n (a_1.node a_2) = Chapter8.S2.depths.frm (n + 1) a_1 ++ Chapter8.S2.depths.frm (n + 1) a_2

@[reducible, inline]

abbrev Chapter8.S2.Weight : Type

Equations

• Chapter8.S2.Weight = ℕ

@[reducible, inline]

abbrev Chapter8.S2.Elem : Type

Equations

• Chapter8.S2.Elem = (Char × Chapter8.S2.Weight)

@[reducible, inline]

abbrev Chapter8.S2.Cost : Type

Equations

• Chapter8.S2.Cost = ℕ

def Chapter8.S2.cost (t : S1.Tree Elem) : Cost

Equations

• Chapter8.S2.cost t = (List.map (fun (x : Chapter8.S2.Elem × ℕ) => match x with | (c, d) => d * c.2) (t.fringe.zip (Chapter8.S2.depths t))).sum

def Chapter8.S2.weight : S1.Tree Elem → ℕ

Equations

• Chapter8.S2.weight (Chapter8.S1.Tree.leaf (fst, w)) = w
• Chapter8.S2.weight (u.node v) = Chapter8.S2.weight u + Chapter8.S2.weight v

def Chapter8.S2.cost₁ : S1.Tree Elem → Cost

Equations

• Chapter8.S2.cost₁ (Chapter8.S1.Tree.leaf a) = 0
• Chapter8.S2.cost₁ (u.node v) = Chapter8.S2.cost u + Chapter8.S2.cost v + Chapter8.S2.weight u + Chapter8.S2.weight v

def Chapter8.S2.pairs {α : Type} (xs : List α) : List ((α × α) × List α)

Equations

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

def Chapter8.S2.insert (t₁ : S1.Tree Elem) : S1.Forest Elem → S1.Forest Elem

Equations

• Chapter8.S2.insert t₁ [] = [t₁]
• Chapter8.S2.insert t₁ (t₂ :: ts) = if Chapter8.S2.weight t₁ ≤ Chapter8.S2.weight t₂ then t₁ :: t₂ :: ts else t₂ :: Chapter8.S2.insert t₁ ts

def Chapter8.S2.combine (ts : S1.Forest Elem) : List (S1.Forest Elem)

Equations

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

def Chapter8.S2.mkForests : List (S1.Tree Elem) → List (S1.Forest Elem)

Equations

• Chapter8.S2.mkForests = Chapter1.until' (flip List.all Chapter1.single) (Chapter1.concatMap Chapter8.S2.combine) ∘ Chapter1.wrap

def Chapter8.S2.mkTrees : List Elem → List (S1.Tree Elem)

Equations

• Chapter8.S2.mkTrees = List.map Chapter1.unwrap! ∘ Chapter8.S2.mkForests ∘ List.map Chapter8.S1.Tree.leaf

def Chapter8.S2.mkForests₁ (ts : List (S1.Tree Elem)) : List (S1.Forest Elem)

Equations

• Chapter8.S2.mkForests₁ ts = Chapter1.apply (ts.length - 1) (Chapter1.concatMap Chapter8.S2.combine) [ts]

def Chapter8.S2.mkTrees₁ : List Elem → List (S1.Tree Elem)

Equations

• Chapter8.S2.mkTrees₁ = List.map Chapter1.unwrap! ∘ Chapter8.S2.mkForests₁ ∘ List.map Chapter8.S1.Tree.leaf

def Chapter8.S2.huffman₁ (es : List Elem) : S1.Tree Elem

Equations

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

@[reducible, inline]

abbrev Chapter8.S2.Queue (α : Type) : Type

Equations

• Chapter8.S2.Queue α = Chapter3.SymList α

@[reducible, inline]

abbrev Chapter8.S2.Stack (α : Type) : Type

Equations

• Chapter8.S2.Stack α = List α

@[reducible, inline]

abbrev Chapter8.S2.SQ (α : Type) : Type

Equations

• Chapter8.S2.SQ α = (Chapter8.S2.Stack α × Chapter8.S2.Queue α)

@[reducible, inline]

abbrev Chapter8.S2.Pair : Type

Equations

• Chapter8.S2.Pair = (Chapter8.S1.Tree Chapter8.S2.Elem × Chapter8.S2.Weight)

def Chapter8.S2.leaf : Elem → Pair

Equations

• Chapter8.S2.leaf (c, w) = (Chapter8.S1.Tree.leaf (c, w), w)

def Chapter8.S2.node : Pair → Pair → Pair

Equations

• Chapter8.S2.node (t₁, w₁) (t₂, w₂) = (t₁.node t₂, w₁ + w₂)

def Chapter8.S2.makeSQ (xs : List Pair) : SQ Pair

Equations

• Chapter8.S2.makeSQ xs = (xs, Chapter3.SymList.nil)

def Chapter8.S2.singleSQ {a : Type} (sq : SQ a) : Bool

Equations

• Chapter8.S2.singleSQ sq = decide (List.isEmpty sq.1 = true ∧ Chapter3.SymList.singleSL sq.2 = true)

def Chapter8.S2.extractSQ (sq : SQ Pair) : S1.Tree Elem

Equations

• Chapter8.S2.extractSQ sq = (Chapter3.SymList.headSL! sq.2).1

def Chapter8.S2.extractMin (ps : SQ Pair) : Pair × SQ Pair

Equations

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

def Chapter8.S2.gstep (ps : SQ Pair) : SQ Pair

Equations

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

def Chapter8.S2.huffman : List Elem → S1.Tree Elem

Equations

• Chapter8.S2.huffman = Chapter8.S2.extractSQ ∘ Chapter1.until' Chapter8.S2.singleSQ Chapter8.S2.gstep ∘ Chapter8.S2.makeSQ ∘ List.map Chapter8.S2.leaf

@[reducible, inline]

abbrev Chapter8.PriorityQueue.Rank : Type

Equations

• Chapter8.PriorityQueue.Rank = ℕ

inductive Chapter8.PriorityQueue.PQ (α β : Type) : Type

• null {α β : Type} : PQ α β
• fork {α β : Type} : Rank → α → β → PQ α β → PQ α β → PQ α β

def Chapter8.PriorityQueue.instReprPQ.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : PQ α✝ β✝ → ℕ → Std.Format

Equations

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

instance Chapter8.PriorityQueue.instReprPQ {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (PQ α✝ β✝)

Equations

• Chapter8.PriorityQueue.instReprPQ = { reprPrec := Chapter8.PriorityQueue.instReprPQ.repr }

def Chapter8.PriorityQueue.instInhabitedPQ.default {a✝ a✝¹ : Type} : PQ a✝ a✝¹

Equations

• Chapter8.PriorityQueue.instInhabitedPQ.default = Chapter8.PriorityQueue.PQ.null

instance Chapter8.PriorityQueue.instInhabitedPQ {a✝ a✝¹ : Type} : Inhabited (PQ a✝ a✝¹)

Equations

• Chapter8.PriorityQueue.instInhabitedPQ = { default := Chapter8.PriorityQueue.instInhabitedPQ.default }

@[irreducible]

def Chapter8.PriorityQueue.mergeOnSnd {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : List (α × β) → List (α × β) → List (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Chapter8.PriorityQueue.mergeOnSnd [] x✝ = x✝
• Chapter8.PriorityQueue.mergeOnSnd x✝ [] = x✝

def Chapter8.PriorityQueue.toListQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : PQ α β → List (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Chapter8.PriorityQueue.toListQ Chapter8.PriorityQueue.PQ.null = []

def Chapter8.PriorityQueue.rank {α β : Type} : PQ α β → Rank

Equations

• Chapter8.PriorityQueue.rank Chapter8.PriorityQueue.PQ.null = 0
• Chapter8.PriorityQueue.rank (Chapter8.PriorityQueue.PQ.fork a a_1 a_2 a_3 a_4) = a

def Chapter8.PriorityQueue.fork {α β : Type} (x : α) (p : β) (t₁ t₂ : PQ α β) : PQ α β

Equations

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

@[irreducible]

def Chapter8.PriorityQueue.combineQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : PQ α β → PQ α β → PQ α β

Equations

• One or more equations did not get rendered due to their size.
• Chapter8.PriorityQueue.combineQ Chapter8.PriorityQueue.PQ.null x✝ = x✝
• Chapter8.PriorityQueue.combineQ x✝ Chapter8.PriorityQueue.PQ.null = x✝

def Chapter8.PriorityQueue.insertQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (x : α) (p : β) (t : PQ α β) : PQ α β

Equations

• Chapter8.PriorityQueue.insertQ x p t = Chapter8.PriorityQueue.combineQ (Chapter8.PriorityQueue.fork x p Chapter8.PriorityQueue.PQ.null Chapter8.PriorityQueue.PQ.null) t

def Chapter8.PriorityQueue.deleteQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (q : PQ α β) (h : q ≠ PQ.null) : (α × β) × PQ α β

Equations

• Chapter8.PriorityQueue.deleteQ Chapter8.PriorityQueue.PQ.null h_2 = absurd ⋯ h_2
• Chapter8.PriorityQueue.deleteQ (Chapter8.PriorityQueue.PQ.fork a x p t₁ t₂) h_2 = ((x, p), Chapter8.PriorityQueue.combineQ t₁ t₂)

def Chapter8.PriorityQueue.deleteQ? {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (q : PQ α β) : Option ((α × β) × PQ α β)

Equations

• Chapter8.PriorityQueue.deleteQ? Chapter8.PriorityQueue.PQ.null = none
• Chapter8.PriorityQueue.deleteQ? (Chapter8.PriorityQueue.PQ.fork a a_1 a_2 a_3 a_4) = some ((a_1, a_2), Chapter8.PriorityQueue.combineQ a_3 a_4)

def Chapter8.PriorityQueue.emptyQ {α β : Type} : PQ α β

Equations

• Chapter8.PriorityQueue.emptyQ = Chapter8.PriorityQueue.PQ.null

def Chapter8.PriorityQueue.nullQ {α β : Type} : PQ α β → Bool

Equations

• Chapter8.PriorityQueue.nullQ Chapter8.PriorityQueue.PQ.null = true
• Chapter8.PriorityQueue.nullQ x✝ = false

def Chapter8.PriorityQueue.addListQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (xs : List (α × β)) (q : PQ α β) : PQ α β

Equations

• Chapter8.PriorityQueue.addListQ xs q = List.foldl (fun (acc : Chapter8.PriorityQueue.PQ α β) (x : α × β) => match x with | (x, p) => Chapter8.PriorityQueue.insertQ x p acc) q xs

def Chapter8.PriorityQueue.makeQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (xs : List (α × β)) : PQ α β

Equations

• Chapter8.PriorityQueue.makeQ xs = Chapter8.PriorityQueue.addListQ xs Chapter8.PriorityQueue.emptyQ

def Chapter8.PriorityQueue.singleQ {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (q : PQ α β) : Bool

Equations

• Chapter8.PriorityQueue.singleQ q = match Chapter8.PriorityQueue.deleteQ? q with | none => true | some (fst, remaining) => Chapter8.PriorityQueue.nullQ remaining

def Chapter8.PriorityQueue.leaf {α β : Type} (x : α) (p : β) : PQ α β

Equations

• Chapter8.PriorityQueue.leaf x p = Chapter8.PriorityQueue.fork x p Chapter8.PriorityQueue.PQ.null Chapter8.PriorityQueue.PQ.null

def Chapter8.PriorityQueue.extract {α β : Type} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (q : PQ α β) : Option α

Equations

• Chapter8.PriorityQueue.extract q = match Chapter8.PriorityQueue.deleteQ? q with | none => none | some ((x, snd), snd_1) => some x

def Chapter8.PriorityQueue.node : S1.Tree S2.Elem × S2.Weight → S1.Tree S2.Elem × S2.Weight → S1.Tree S2.Elem × S2.Weight

Equations

• Chapter8.PriorityQueue.node (t₁, w₁) (t₂, w₂) = (t₁.node t₂, w₁ + w₂)

def Chapter8.PriorityQueue.gstep (ps : PQ (S1.Tree S2.Elem) S2.Weight) : PQ (S1.Tree S2.Elem) S2.Weight

Equations

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

def Chapter8.PriorityQueue.huffmanPQ (es : List S2.Elem) : Option (S1.Tree S2.Elem)

Equations

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

def Chapter8.PriorityQueue.pqInsert1 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqInsert1 = Chapter8.PriorityQueue.insertQ 5 3 Chapter8.PriorityQueue.emptyQ

def Chapter8.PriorityQueue.pqInsert2 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqInsert2 = Chapter8.PriorityQueue.insertQ 2 1 Chapter8.PriorityQueue.pqInsert1

def Chapter8.PriorityQueue.pqInsert3 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqInsert3 = Chapter8.PriorityQueue.insertQ 8 4 Chapter8.PriorityQueue.pqInsert2

def Chapter8.PriorityQueue.pqAfterDelete1 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqAfterDelete1 = match Chapter8.PriorityQueue.deleteQ? Chapter8.PriorityQueue.pqInsert3 with | some (fst, q) => q | none => Chapter8.PriorityQueue.emptyQ

def Chapter8.PriorityQueue.pqAfterDelete2 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqAfterDelete2 = match Chapter8.PriorityQueue.deleteQ? Chapter8.PriorityQueue.pqAfterDelete1 with | some (fst, q) => q | none => Chapter8.PriorityQueue.emptyQ

def Chapter8.PriorityQueue.pqMake1 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqMake1 = Chapter8.PriorityQueue.makeQ [(5, 3), (2, 1), (8, 4)]

def Chapter8.PriorityQueue.pqMake2 : PQ String ℕ

Equations

• Chapter8.PriorityQueue.pqMake2 = Chapter8.PriorityQueue.makeQ [("baixa", 5), ("urgente", 1), ("normal", 3)]

def Chapter8.PriorityQueue.initialQueue : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.initialQueue = Chapter8.PriorityQueue.insertQ 10 5 Chapter8.PriorityQueue.emptyQ

def Chapter8.PriorityQueue.elementsToAdd : List (ℕ × ℕ)

Equations

• Chapter8.PriorityQueue.elementsToAdd = [(3, 1), (7, 4), (2, 2), (9, 6)]

def Chapter8.PriorityQueue.finalQueue : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.finalQueue = Chapter8.PriorityQueue.addListQ Chapter8.PriorityQueue.elementsToAdd Chapter8.PriorityQueue.initialQueue

def Chapter8.PriorityQueue.pq1 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pq1 = Chapter8.PriorityQueue.makeQ [(2, 1), (5, 3)]

def Chapter8.PriorityQueue.pq2 : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pq2 = Chapter8.PriorityQueue.makeQ [(1, 0), (8, 4)]

def Chapter8.PriorityQueue.pqCombined : PQ ℕ ℕ

Equations

• Chapter8.PriorityQueue.pqCombined = Chapter8.PriorityQueue.combineQ Chapter8.PriorityQueue.pq1 Chapter8.PriorityQueue.pq2