def isEven (n : ℕ) : Bool

Equations

• isEven n = (2 * (n / 2) == n)

theorem isEvenProof (n : ℕ) (p : isEven n = true) : n = n / 2 + n / 2

theorem isOddProof (n : ℕ) (p : ¬isEven n = true) : n = n / 2 + n / 2 + 1

def emptyLeaf {α β : Type} : ABTree (Option α) β

Equations

• emptyLeaf = ABTree.leaf none

def single {α : Type} (a : α) : ABTree (Option α) α

Equations

• single a = ABTree.node a emptyLeaf emptyLeaf

def infixSeq {α : Type} (t : ABTree α α) : Sequence t.size α

Equations

• infixSeq (ABTree.leaf v) = Sequence.single v
• infixSeq (ABTree.node a bl br) = sequence_coerce ⋯ ((infixSeq bl).append (Sequence.cons a (infixSeq br)))

@[irreducible]

def seqHABTree {α : Type} {n : ℕ} (seq : Sequence n α) : ABTree (Option α) α

Equations

• seqHABTree seq_2 = ABTree.leaf none
• seqHABTree seq_2 = ABTree.leaf (some seq_2.head)
• seqHABTree seq_2 = ABTree.node ((Sequence.drop (ppn / 2).succ seq_2).head' ⋯) (seqHABTree (Sequence.take (ppn / 2).succ ⋯ seq_2)) (seqHABTree (Sequence.drop (ppn / 2).succ.succ seq_2))

def perfectSeq {α : Type} {n : ℕ} (seq : Sequence (2 ^ n.succ - 1) α) : ABTree α α

Equations

• perfectSeq seq_2 = ABTree.leaf seq_2.head
• perfectSeq seq_2 = match seq_2.perfect_split with | (seql, ar, seqr) => ABTree.node ar (perfectSeq seql) (perfectSeq seqr)

def perfectSeqLeaves {α : Type} {n : ℕ} (seq : Sequence (2 ^ n) α) : BTree α

Equations

• perfectSeqLeaves seq_2 = BTree.leaf seq_2.head
• perfectSeqLeaves seq_2 = match half_split_pow seq_2 with | (lseq, rseq) => (perfectSeqLeaves lseq).node (perfectSeqLeaves rseq)

theorem perfect_tree_size {α : Type} {n : ℕ} (seq : Sequence (2 ^ n.succ - 1) α) : (perfectSeq seq).size = 2 ^ n.succ - 1

theorem seq_tree_seq {α : Type} {n : ℕ} (seq : Sequence (2 ^ n.succ - 1) α) : infixSeq (perfectSeq seq) = sequence_coerce ⋯ seq

def gen_empty_perfect_tree : ℕ → ABTree Unit Unit

Equations

• gen_empty_perfect_tree Nat.zero = ABTree.leaf ()
• gen_empty_perfect_tree pn.succ = ABTree.node () (gen_empty_perfect_tree pn) (gen_empty_perfect_tree pn)

def gen_info_perfect_tree {α β : Type} {h : ℕ} (nodes : Sequence (2 ^ h - 1) β) (leaves : Sequence (2 ^ h) α) : ABTree α β

Equations

• One or more equations did not get rendered due to their size.
• gen_info_perfect_tree nodes_2 leaves_2 = ABTree.leaf leaves_2.head

theorem take_init {α : Type} {n m : ℕ} (hLT : m.succ ≤ n) (s : Sequence n α) : (Sequence.take m.succ hLT s).init = Sequence.take m ⋯ s

theorem take_less_init {α : Type} {n k m : ℕ} (hLT : m < n) (heq : n = k + 1) (s : Sequence n α) : Sequence.take m ⋯ (sequence_coerce heq s).init = Sequence.take m ⋯ s

theorem half_perfect_split_same {α : Type} {n : ℕ} (s : Sequence (2 ^ n.succ) α) : (sequence_coerce ⋯ (half_split_pow s).1).init = (sequence_coerce ⋯ s).init.perfect_split.1

theorem take_constant {α : Type} {n m : ℕ} {mLt : m ≤ n} {a : α} : Sequence.take m mLt (Sequence.constant n a) = Sequence.constant m a

theorem perfect_split_constant {α : Type} {lgn : ℕ} (a : α) : Sequence.constant (2 ^ lgn - 1) a = (Sequence.constant (2 ^ lgn.succ - 1) a).perfect_split.1

theorem gen_empty_size {n : ℕ} : (gen_empty_perfect_tree n).size = 2 ^ n.succ - 1