def comb_tree_heterogeneous {α β : Type} (lf : α → β) (f : β → β → β) (p q : ABTree α β) : ABTree α β

Equations

• comb_tree_heterogeneous lf f p q = ABTree.node (f (ABTree.getI' lf id p) (ABTree.getI' lf id q)) p q

def comb_tree_homogeneous {α : Type} (f : α → α → α) (p q : ABTree α α) : ABTree α α

Equations

• comb_tree_homogeneous f p q = ABTree.node (f p.hget q.hget) p q

def game_arena {lgn : ℕ} (skl : Sequence (2 ^ lgn) SkElem) : ABTree SkElem Unit

Equations

• game_arena skl = Sequence.consume_pow (comb_tree_heterogeneous (fun (x : SkElem) => ()) fun (x x : Unit) => ()) (Sequence.map ABTree.leaf skl)

def get_spine {α : Type} (side : SkElem) (e : α × α) : α

Equations

• get_spine SkElem.Left e = e.1
• get_spine SkElem.Right e = e.2

def get_sibling {α : Type} (side : SkElem) (e : α × α) : α

Equations

• get_sibling SkElem.Left e = e.2
• get_sibling SkElem.Right e = e.1

def extract_intermed_hashes {ℍ : Type} {n : ℕ} (skl : Sequence n SkElem) (prop : Sequence n (ℍ × ℍ)) : Sequence n ℍ

Equations

• extract_intermed_hashes skl prop = Sequence.zip_with get_spine skl prop

def extract_sibling_hashes {ℍ : Type} {n : ℕ} (skl : Sequence n SkElem) (prop : Sequence n (ℍ × ℍ)) : Sequence n ℍ

Equations

• extract_sibling_hashes skl prop = Sequence.zip_with get_sibling skl prop

def built_up_arena {n : ℕ} : Sequence (2 ^ n) SkElem → ABTree SkElem Unit

Equations

• built_up_arena = gen_info_perfect_tree (Sequence.constant (2 ^ n - 1) ())

def built_up_arena_backward {n : ℕ} : Sequence (2 ^ n) SkElem → ABTree SkElem Unit

Equations

• built_up_arena_backward = gen_info_perfect_tree (Sequence.constant (2 ^ n - 1) ()) ∘ Sequence.reverse

def backward_proposer_to_tree {α : Type} {n : ℕ} (sides : Sequence (2 ^ n) SkElem) (prop : Sequence (2 ^ n) (α × α)) : ABTree α α

Equations

• backward_proposer_to_tree sides prop = gen_info_perfect_tree (sequence_coerce ⋯ (extract_intermed_hashes sides prop)).init.reverse (extract_sibling_hashes sides prop).reverse

def forward_proposer_to_tree {α : Type} {n : ℕ} (prop : Sequence (2 ^ n) (α × α)) : ABTree α α

Equations

• forward_proposer_to_tree prop = gen_info_perfect_tree (sequence_coerce ⋯ (Sequence.map (fun (p : α × α) => p.1) prop)).init (Sequence.map (fun (p : α × α) => p.2) prop)

theorem proposer_winning_conditions {ℍ : Type} {lgn : ℕ} [BEq ℍ] [LawfulBEq ℍ] [m : HashMagma ℍ] {da : ElemInTreeH (2 ^ lgn) ℍ} {proposer : Sequence (2 ^ lgn) (ℍ × ℍ)} (wProp : elem_in_reveler_winning_condition_backward da proposer) : reveler_winning_condition_simp_game (fun (x : Range ℍ) (c : ℍ) => match x with | (a, b) => ((a, c), c, b)) (fun (s : SkElem) (h : ℍ) (rh : Range ℍ) => winning_proposer (leaf_condition_length_one s h rh)) (fun (x : Unit) (x : ℍ) (x : Range ℍ) => Player.Proposer) { data := built_up_arena_backward da.data, res := da.mtree } (ABTree.map some some (backward_proposer_to_tree da.data proposer))

theorem proposer_winning_mod {ℍ : Type} {lgn : ℕ} [BEq ℍ] [LawfulBEq ℍ] [HashMagma ℍ] (da : ElemInTreeH (2 ^ lgn) ℍ) (proposer : Sequence (2 ^ lgn) (ℍ × ℍ)) (wProp : elem_in_reveler_winning_condition_backward da proposer) (chooser : ABTree Unit (Range ℍ → ℍ → Option ChooserMoves)) : spl_game { data := built_up_arena_backward da.data, res := da.mtree } (ABTree.map some some (backward_proposer_to_tree da.data proposer)) chooser = Player.Proposer

theorem proposer_winning_mod_forward {ℍ : Type} {lgn : ℕ} [BEq ℍ] [LawfulBEq ℍ] [HashMagma ℍ] (da : ElemInTreeH (2 ^ lgn) ℍ) (proposer : Sequence (2 ^ lgn) (ℍ × ℍ)) (wProp : elem_in_reveler_winning_condition_forward da proposer) (chooser : ABTree Unit (Range ℍ → ℍ → Option ChooserMoves)) : spl_game { data := built_up_arena da.data, res := da.mtree } (ABTree.map some some (forward_proposer_to_tree proposer)) chooser = Player.Proposer