inductive SimWinner : Type

• Left : SimWinner
• Right : SimWinner

def leaf_game {α ℍ : Type} [DecidableEq ℍ] [o : Hash α ℍ] (a : α) (p commit : ℍ) : SimWinner

Equations

• leaf_game a p commit = if o.mhash a = p ∧ commit = p then SimWinner.Left else SimWinner.Right

def node_game {ℍ : Type} [DecidableEq ℍ] [mag : HashMagma ℍ] (lp rp : ℍ × ℍ) (commit : ℍ) (recl recr : SimWinner) : SimWinner

Equations

• node_game lp rp commit recl recr = if lp = rp then if mag.comb lp.1 lp.2 = commit then SimWinner.Left else SimWinner.Right else if ¬lp.1 = rp.1 then recl else recr

def simultaneous_game {α ℍ : Type} [o : Hash α ℍ] [mag : HashMagma ℍ] [DecidableEq ℍ] (public_data : ABTree ℍ Unit) (lplayer : ABTree (Option α) (Option (ℍ × ℍ))) (lplayer_commit : ℍ) (rplayer : ABTree Unit (Option (ℍ × ℍ))) : SimWinner

Equations

• One or more equations did not get rendered due to their size.
• simultaneous_game (ABTree.leaf p) (ABTree.leaf none) lplayer_commit rplayer = SimWinner.Right
• simultaneous_game (ABTree.leaf p) (ABTree.leaf (some llp)) lplayer_commit rplayer = leaf_game llp p lplayer_commit
• simultaneous_game (ABTree.node i gl gr) (ABTree.node none ll lr) lplayer_commit (ABTree.node rp rl rr) = SimWinner.Right
• simultaneous_game (ABTree.node i gl gr) (ABTree.node lp ll lr) lplayer_commit (ABTree.node none rl rr) = SimWinner.Left
• simultaneous_game (ABTree.leaf v) (ABTree.node i bL bR) lplayer_commit rplayer = SimWinner.Right
• simultaneous_game (ABTree.node i bL bR) (ABTree.leaf v) lplayer_commit rplayer = SimWinner.Right
• simultaneous_game (ABTree.node i bL bR) (ABTree.node (some val) bL_1 bR_1) lplayer_commit (ABTree.leaf v) = SimWinner.Left
• simultaneous_game (ABTree.node i bL bR) (ABTree.node none bL_1 bR_1) lplayer_commit (ABTree.leaf v) = SimWinner.Right

def gen_to_chooser {ℍ : Type} [DecidableEq ℍ] (md : Option (ℍ × ℍ)) (a : ℍ × ℍ × ℍ) : Option ChooserMoves

Equations

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

theorem eq_sim_games {α ℍ : Type} [o : Hash α ℍ] [mag : HashMagma ℍ] [DecidableEq ℍ] (pub : ABTree ℍ Unit) (lplayer : ABTree (Option α) (Option (ℍ × ℍ))) (lplayer_commit : ℍ) (rplayer : ABTree Unit (Option (ℍ × ℍ))) : treeArbitrationGame { computation := pub, res := lplayer_commit } lplayer (ABTree.map id gen_to_chooser rplayer) = Player.Proposer ↔ simultaneous_game pub lplayer lplayer_commit rplayer = SimWinner.Left

def simultaneous_elemenin_game {α ℍ : Type} [o : Hash α ℍ] [mag : HashMagma ℍ] [DecidableEq ℍ] (public_data : ABTree SkElem Unit) (lplayer : ABTree (Option α) (Option ℍ)) (lplayer_commit : ℍ × ℍ) (rplayer : ABTree Unit (Option ℍ)) : SimWinner

Equations

• One or more equations did not get rendered due to their size.
• simultaneous_elemenin_game (ABTree.leaf side) (ABTree.leaf none) lplayer_commit (ABTree.leaf _rp) = SimWinner.Right
• simultaneous_elemenin_game (ABTree.node i gl gr) (ABTree.node none ll lr) lplayer_commit (ABTree.node rp rl rr) = SimWinner.Right
• simultaneous_elemenin_game (ABTree.node i gl gr) (ABTree.node lp ll lr) lplayer_commit (ABTree.node none rl rr) = SimWinner.Left
• simultaneous_elemenin_game (ABTree.leaf v) (ABTree.node i bL bR) lplayer_commit rplayer = SimWinner.Right
• simultaneous_elemenin_game (ABTree.leaf v) lplayer lplayer_commit (ABTree.node i bL bR) = SimWinner.Left
• simultaneous_elemenin_game (ABTree.node i bL bR) (ABTree.leaf v) lplayer_commit rplayer = SimWinner.Right
• simultaneous_elemenin_game (ABTree.node i bL bR) lplayer lplayer_commit (ABTree.leaf v) = SimWinner.Left