Exercicio 4.5

Indexing the coordinates from zero, the positions are (0, 9), (5, 6), (7, 5), (9, 0)

def Chapter4.BST1.flatcat {a : Type} (t : Tree a) (xs : List a) : List a

Equations

• Chapter4.BST1.flatcat Chapter4.BST1.Tree.null x✝ = x✝
• Chapter4.BST1.flatcat (l.node x_2 r) x✝ = Chapter4.BST1.flatcat l (x_2 :: Chapter4.BST1.flatcat r x✝)

def Chapter4.BST1.Tree.flatten₁ {a : Type} (t : Tree a) : List a

Equations

• t.flatten₁ = Chapter4.BST1.flatcat t []

def Chapter4.partition {α : Type} (p : α → Bool) : List α → List α × List α

Equations

• Chapter4.partition p = List.foldr (fun (x : α) (r : List α × List α) => if p x = true then (x :: r.fst, r.snd) else (r.fst, x :: r.snd)) ([], [])

def Chapter4.BST2.partition3 {a : Type u_1} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] [DecidableRel fun (x1 x2 : a) => x1 = x2] (y : a) (xs : List a) : List a × List a × List a

Equations

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

partial def Chapter4.BST2.mkTree₃ (xs : List Nat) : Tree (List Nat)

@[irreducible]

def Chapter4.DSet.merge {a : Type u_1} [LT a] [DecidableEq a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a → List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.DSet.merge [] x✝ = x✝
• Chapter4.DSet.merge x✝ [] = x✝

def Chapter4.DSet.union₁ {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (t₁ t₂ : Set a) : Set a

Equations

• Chapter4.DSet.union₁ t₁ t₂ = List.foldr Chapter4.BST2.insert t₁ (Chapter4.BST2.Tree.flatten t₂)

partial def Chapter4.DSet.frm {a : Type} [Inhabited a] (l r : Nat) (xa : Array a) : Set a

def Chapter4.DSet.build {a : Type} [Inhabited a] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (xs : List a) : Set a

Equations

• Chapter4.DSet.build xs = Chapter4.DSet.frm 0 xs.length xs.toArray

def Chapter4.DSet.union₂ {a : Type} [Inhabited a] [LT a] [DecidableEq a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (t₁ t₂ : Set a) : Set a

Equations

• Chapter4.DSet.union₂ t₁ t₂ = Chapter4.DSet.build (Chapter4.DSet.merge (Chapter4.BST2.Tree.flatten t₁) (Chapter4.BST2.Tree.flatten t₂))

def Chapter4.DSet.pair {α β : Type} (f : α → β) (p : α × α) : β × β

Equations

• Chapter4.DSet.pair f p = (f p.fst, f p.snd)

def Chapter4.DSet.split₁ {α : Type} [LT α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 < x2] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Set α → Set α × Set α

Equations

• Chapter4.DSet.split₁ x = Chapter4.DSet.pair Chapter4.BST2.mkTree ∘ (List.partition fun (x_1 : α) => decide (x_1 ≤ x)) ∘ Chapter4.BST2.Tree.flatten