structure ElemInMTree (α ℍ : Type) : Type

• elem : α
• path : Skeleton
• mtree : ℍ

def implicit_element_in_tree {α ℍ : Type} [m : Hash α ℍ] [mag : HashMagma ℍ] (computation : ElemInMTree α ℍ) (missing_data : List ℍ) : Prop

Equations

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

def leaf_condition {α ℍ : Type} [BEq ℍ] [o : Hash α ℍ] (a : α) (h : ℍ) : Winner

Equations

• leaf_condition a h = winning_proposer (o.mhash a == h)

def mid_condition {ℍ : Type} [BEq ℍ] [mag : HashMagma ℍ] (p : PMoves ℍ) (h : ℍ) : Winner

Equations

• mid_condition p h = winning_proposer (mag.comb p.1 p.2 == h)

@[irreducible]

def arbElem {α ℍ : Type} (pos : Skeleton) [BEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] (da : ElemInMTree α ℍ) (proposer : Skeleton → Option (PMoves ℍ)) (chooser : Skeleton → PMoves ℍ → Option ChooserSmp) : Winner

Equations

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

def arbElemInit {α ℍ : Type} [BEq ℍ] [Hash α ℍ] [HashMagma ℍ] (da : ElemInMTree α ℍ) (proposer : Skeleton → Option (PMoves ℍ)) (chooser : Skeleton → PMoves ℍ → Option ChooserSmp) : Winner

Equations

• arbElemInit da proposer chooser = arbElem [] da proposer chooser

structure ElemInTreeN (n : ℕ) (α ℍ : Type) : Type

• data : α × ISkeleton n
• mtree : ℍ

def SingleLastStep {α ℍ : Type} [BEq ℍ] [h : Hash α ℍ] (data : ElemInTreeN 0 α ℍ) : Winner

Equations

• SingleLastStep data = winning_proposer (h.mhash data.data.1 == data.mtree)

def SingleMidStep {ℍ : Type} [BEq ℍ] [m : HashMagma ℍ] (data : ℍ × ℍ × ℍ) : Winner

Equations

• SingleMidStep data = winning_proposer (m.comb data.2.1 data.2.2 == data.1)

def elemInHGame {α ℍ : Type} [BEq ℍ] [Hash α ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeN 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.
• elemInHGame da_2 proposer_2 chooser_2 = SingleLastStep da_2

structure ElemInTreeH (n : ℕ) (ℍ : Type) : Type

• data : ISkeleton n
• mtree : ℍ × ℍ

def SingleLastStepH {ℍ : Type} [BEq ℍ] (data : ElemInTreeH 0 ℍ) : Winner

Equations

• SingleLastStepH data = winning_proposer (data.mtree.1 == data.mtree.2)

def elem_in_tree_backward {ℍ : Type} [BEq ℍ] [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.
• elem_in_tree_backward da_2 proposer_2 chooser_2 = SingleLastStepH da_2

def forward_mid_step_condition {ℍ : Type} [BEq ℍ] [m : HashMagma ℍ] (side : SkElem) (data : ℍ × ℍ) (res : ℍ) : Winner

Equations

• forward_mid_step_condition side data res = winning_proposer (op_side side data.1 data.2 == res)

def elem_in_tree_forward {ℍ : Type} [BEq ℍ] [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.
• elem_in_tree_forward da_2 proposer_2 chooser_2 = SingleLastStepH da_2

def elem_in_forward {α ℍ : Type} {n : ℕ} [BEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] (path : ISkeleton n) (elem : α) (top : ℍ) (proposer : Sequence n (Option (ℍ × ℍ))) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : Winner

Equations

• elem_in_forward path elem top proposer chooser = elem_in_tree_forward { data := path, mtree := (o.mhash elem, top) } proposer chooser

def elem_in_backward_rev {α ℍ : Type} {n : ℕ} [BEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] (path : ISkeleton n) (top : ℍ) (proposer : Sequence n (Option (ℍ × ℍ)) × Option α) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : Winner × Option α

Equations

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

def naive_lin_forward_test {ℍ : Type} [m : HashMagma ℍ] [BEq ℍ] : ℍ × ℍ × ℍ → Option ChooserSmp

Equations

• naive_lin_forward_test (top, hl, hr) = some (if (m.comb hl hr == top) = true then ChooserPrimMoves.Continue () else ChooserPrimMoves.Now)

def naive_lin_forward {ℍ : Type} {n : ℕ} [HashMagma ℍ] [BEq ℍ] : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)

Equations

• naive_lin_forward = Sequence.constant n naive_lin_forward_test

theorem elem_back_rev_honest_two {α ℍ : Type} {n : ℕ} [DecidableEq α] [BEq ℍ] [LawfulBEq ℍ] [H : Hash α ℍ] [Mag : HashMagma ℍ] [injH : InjectiveHash α ℍ] [injM : InjectiveMagma ℍ] {ph : ISkeleton n} {mk : ℍ} {e : α} (proposer : Sequence n (Option (ℍ × ℍ)) × Option α) {data : BTree α} (HMkTree : data.hash_BTree = mk) (HElem : ABTree.iaccess data ph = some (Sum.inl e)) : elem_in_backward_rev ph mk proposer naive_lin_forward = (Player.Proposer, some e) ∨ elem_in_backward_rev ph mk proposer naive_lin_forward = (Player.Chooser, none)

def elem_in_reveler_winning_condition_backward {ℍ : Type} [BEq ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (PMoves ℍ)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• elem_in_reveler_winning_condition_backward da_2 proposer_2 = (SingleLastStepH da_2 = Player.Proposer)

def elem_in_reveler_winning_condition_forward {ℍ : Type} [BEq ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (ℍ × ℍ)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• elem_in_reveler_winning_condition_forward da_2 proposer_2 = (SingleLastStepH da_2 = Player.Proposer)

def spine_forward {ℍ : Type} {n : ℕ} : Sequence n (PMoves ℍ) → Sequence n ℍ

Equations

• spine_forward = Sequence.map fun (p : PMoves ℍ) => p.1

def sibling_forward {ℍ : Type} {n : ℕ} : Sequence n (PMoves ℍ) → Sequence n ℍ

Equations

• sibling_forward = Sequence.map fun (p : PMoves ℍ) => p.2

theorem winning_reveler_wins {ℍ : Type} [BEq ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (PMoves ℍ)) (winning_prop : elem_in_reveler_winning_condition_backward da proposer) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : elem_in_tree_backward da (Sequence.map some proposer) chooser = Player.Proposer

theorem winning_reveler_wins_forward {ℍ : Type} [BEq ℍ] [HashMagma ℍ] {n : ℕ} (da : ElemInTreeH n ℍ) (proposer : Sequence n (PMoves ℍ)) (winning_prop : elem_in_reveler_winning_condition_forward da proposer) (chooser : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : elem_in_tree_forward da (Sequence.map some proposer) chooser = Player.Proposer

def last_step {ℍ : Type} [BEq ℍ] [m : HashMagma ℍ] (side : SkElem) (res : ℍ) (data : ℍ × ℍ) : Winner

Equations

• last_step side res data = winning_proposer (op_side side data.1 res == data.2)

def knowing {ℍ : Type} [BEq ℍ] [HashMagma ℍ] (skl : ABTree SkElem Unit) (know : ABTree ℍ ℍ) (i o : ℍ) : Prop

Equations

• knowing (ABTree.leaf sk) (ABTree.leaf h) i o = (op_side sk i h = o)
• knowing (ABTree.node i_1 al ar) (ABTree.node mid kl kr) i o = (knowing al kl i mid ∧ knowing ar kr mid o)
• knowing skl know i o = False

def input_prop {ℍ : Type} (data : ABTree (Option ℍ) (Option ℍ)) (i : ℍ) : Prop

Equations

• input_prop (ABTree.node i_1 bl bR) i = input_prop bl i
• input_prop (ABTree.leaf (some h)) i = (h = i)
• input_prop (ABTree.leaf none) i = False

theorem range_chooser_wins {ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [HashMagma ℍ] [hash_props : SLawFulHash ℍ] (comp_skeleton : ABTree SkElem Unit) (input_rev input_ch output : ℍ) (hneq : ¬input_rev = input_ch) (reveler : ABTree (Option ℍ) (Option ℍ)) (chooser : ABTree ℍ ℍ) (chooser_wise : knowing comp_skeleton chooser input_ch output) : spl_game { data := comp_skeleton, res := (input_rev, output) } reveler (gen_to_fun_chooser (ABTree.map some some chooser)) = Player.Chooser