def skl_to_tree {n : ℕ} (sk : ISkeleton n) : ABTree Unit Unit

Equations

• One or more equations did not get rendered due to their size.
• skl_to_tree sk_2 = ABTree.leaf ()

def skl_to_maybe_elem {α : Type} {n : ℕ} (a : α) (sk : ISkeleton n) : ABTree (Option α) Unit

Equations

• One or more equations did not get rendered due to their size.
• skl_to_maybe_elem a sk_2 = ABTree.leaf (some a)

def build_proposer' {ℍ : Type} {n : ℕ} (bot_hash : ℍ) (skl : ISkeleton n) (rev : Sequence n (Option (PMoves ℍ))) : ABTree (Option ℍ) (Option (Range ℍ × Range ℍ))

Equations

• One or more equations did not get rendered due to their size.
• build_proposer' bot_hash skl_2 rev_2 = ABTree.leaf (some bot_hash)

def build_proposer {ℍ : Type} {n : ℕ} (data : ℍ × ISkeleton n) (rev : Sequence n (Option (PMoves ℍ))) : ABTree (Option ℍ) (Option (ℍ × ℍ))

Equations

• One or more equations did not get rendered due to their size.
• build_proposer data_2 rev_2 = ABTree.leaf (some data_2.1)

def build_chooser {ℍ : Type} {n : ℕ} (data : ℍ × ISkeleton n) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : ABTree Unit (ℍ × ℍ × ℍ → Option ChooserMoves)

Equations

• One or more equations did not get rendered due to their size.
• build_chooser data_2 chooser_2 = ABTree.leaf ()

def build_chooser' {ℍ : Type} {n : ℕ} (skl : ISkeleton n) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : ABTree Unit ((ℍ × ℍ) × (ℍ × ℍ) × ℍ × ℍ → Option ChooserMoves)

Equations

• One or more equations did not get rendered due to their size.
• build_chooser' skl_2 chooser_2 = ABTree.leaf ()

def elem_in_tree_gen_tree {ℍ : Type} [BEq ℍ] [mag : HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (Option (PMoves ℍ))) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : Winner

Equations

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

def elem_in_tree_forward_gentree {ℍ : Type} [BEq ℍ] [mag : HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (Option (PMoves ℍ))) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : Winner

Equations

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

theorem seq_equiv_tree {ℍ : Type} [BEq ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (Option (PMoves ℍ))) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : elem_in_tree_backward da proposer chooser = elem_in_tree_gen_tree da proposer chooser