Equations
- dac_node_winning_condition top hl hr = (m.comb hl hr == top)
Instances For
theorem
dac_winning_gen_chooser
{α ℍ : Type}
[hash : Hash α ℍ]
[HashMagma ℍ]
[BEq ℍ]
[LawfulBEq ℍ]
(pub_data : ABTree ℍ Unit)
(revealer : ABTree (Option α) (Option (ℍ × ℍ)))
(rev_res : ℍ)
(chooser : ABTree (Option α) (Option (ℍ × ℍ)))
(ch_res : ℍ)
(good_chooser :
winning_condition_player (fun (hc : ℍ) (a : α) (h : ℍ) => dac_leaf_winning_condition hc a h = true)
(fun (x : Unit) (x : ℍ × ℍ) (res : ℍ) =>
match x with
| (l, r) => dac_node_winning_condition res l r = true)
(fun (x : ℍ) => id) { data := pub_data, res := ch_res } chooser)
(hneq : ¬rev_res = ch_res)
:
data_challenge_game { computation := pub_data, res := rev_res } revealer
(ABTree.map (fun (x : Option α) => ()) gen_chooser_opt chooser) = Player.Chooser
def
arbitrationTree
{α ℍ : Type}
[BEq ℍ]
[o : Hash α ℍ]
[m : HashMagma ℍ]
(arena : ABTree Unit Unit)
(res : ℍ)
(reveler : ABTree (Option α) (Option (ℍ × ℍ)))
(chooser : ABTree Unit (ℍ × ℍ × ℍ → Option ChooserMoves))
:
Equations
- One or more equations did not get rendered due to their size.