def cond_hash_elem {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [h : Hash α ℍ] (leaf : ℍ) (rev : α) (res : ℍ) : Bool

Equations

• cond_hash_elem leaf rev res = (h.mhash rev == res && leaf == res)

def cond_hash {ℍ : Type} [BEq ℍ] [mag : HashMagma ℍ] (res l r : ℍ) : Bool

Equations

• cond_hash res l r = (mag.comb l r == res)

@[reducible, inline]

abbrev dac_game {ℍ α : Type} [BEq ℍ] [LawfulBEq ℍ] [Hash α ℍ] [HashMagma ℍ] (da : CompTree ℍ Unit ℍ) (revealer : ABTree (Option α) (Option (ℍ × ℍ))) (chooser : ABTree Unit (ℍ × ℍ × ℍ → Option ChooserMoves)) : Winner

Equations

• dac_game da revealer chooser = treeCompArbGame cond_hash_elem (fun (x : Unit) => cond_hash) da revealer chooser

theorem winning_prop_hashes {ℍ α : Type} [DecidableEq ℍ] [Hash α ℍ] [HashMagma ℍ] (da : CompTree ℍ Unit ℍ) (revealer : ABTree (Option α) (Option (ℍ × ℍ))) (good_revealer : reveler_winning_condition cond_hash_elem (fun (x : Unit) => cond_hash) da revealer) (chooser : ABTree Unit (ℍ × ℍ × ℍ → Option ChooserMoves)) : treeCompArbGame cond_hash_elem (fun (x : Unit) => cond_hash) da revealer chooser = Player.Proposer

theorem winning_gen_chooser {ℍ α : Type} [hash : Hash α ℍ] [HashMagma ℍ] [DecidableEq ℍ] (pub_data : ABTree ℍ Unit) (revealer : ABTree (Option α) (Option (ℍ × ℍ))) (rev_res : ℍ) (chooser : ABTree (Option α) (Option (ℍ × ℍ))) (ch_res : ℍ) (good_chooser : winning_condition_player (fun (c : ℍ) (a : α) (h : ℍ) => cond_hash_elem c a h = true) (fun (x : Unit) (x : ℍ × ℍ) (res : ℍ) => match x with | (l, r) => cond_hash res l r = true) (fun (x : ℍ) => id) { data := pub_data, res := ch_res } chooser) (hneq : ¬rev_res = ch_res) : treeCompArbGame cond_hash_elem (fun (x : Unit) => cond_hash) { data := pub_data, res := rev_res } revealer (ABTree.map (fun (x : Option α) => ()) gen_chooser_opt chooser) = Player.Chooser