@[reducible, inline]

abbrev Range (ℍ : Type) : Type

Equations

• Range ℍ = (ℍ × ℍ)

def all_true (ls : List Bool) : Bool

Equations

• all_true ls = ls.all id

def leaf_condition_range {ℍ : Type} [BEq ℍ] (_k : Unit) (h : ℍ) (hda : ℍ × ℍ) : Bool

Equations

• leaf_condition_range _k h hda = all_true [h == hda.1, hda.1 == hda.2]

def mid_condition_range_one_step_forward {ℍ : Type} [BEq ℍ] [m : HashMagma ℍ] : Unit → Range ℍ → Range ℍ → Range ℍ → Bool

Equations

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

structure CompTree (α β γ : Type) : Type

• data : ABTree α β
• res : γ

def simp_tree {α α' β β' γ : Type} (splitter : γ → β → γ × γ) (leafCondition : α' → α → γ → Winner) (midCondition : β' → β → γ → Winner) (da : CompTree α' β' γ) (reveler : ABTree (Option α) (Option β)) (chooser : ABTree Unit (γ → β → Option ChooserMoves)) : Winner

Equations

• One or more equations did not get rendered due to their size.
• simp_tree splitter leafCondition midCondition da (ABTree.leaf (some a)) chooser = leafCondition h a da.res
• simp_tree splitter leafCondition midCondition da (ABTree.node (some proposition) nextProposerLeft nextProposerRight) chooser = Player.Proposer
• simp_tree splitter leafCondition midCondition da reveler✝ chooser = Player.Chooser

def reveler_winning_condition_simp_game {α α' β β' γ : Type} (splitter : γ → β → γ × γ) (leafCondition : α' → α → γ → Winner) (midCondition : β' → β → γ → Winner) (da : CompTree α' β' γ) (reveler : ABTree (Option α) (Option β)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• reveler_winning_condition_simp_game splitter leafCondition midCondition da (ABTree.leaf (some a')) = (leafCondition a a' da.res = Player.Proposer)
• reveler_winning_condition_simp_game splitter leafCondition midCondition da reveler✝ = False

theorem simp_game_reveler_wins {α α' β β' γ : Type} (splitter : γ → β → γ × γ) (leafCondition : α' → α → γ → Winner) (midCondition : β' → β → γ → Winner) (da : CompTree α' β' γ) (reveler : ABTree (Option α) (Option β)) (wProp : reveler_winning_condition_simp_game splitter leafCondition midCondition da reveler) (chooser : ABTree Unit (γ → β → Option ChooserMoves)) : simp_tree splitter leafCondition midCondition da reveler chooser = Player.Proposer

def treeCompArbGame {α α' β γ : Type} (leafCondition : α → α' → γ → Bool) (midCondition : β → γ → γ → γ → Bool) (da : CompTree α β γ) (reveler : ABTree (Option α') (Option (γ × γ))) (chooser : ABTree Unit (γ × γ × γ → Option ChooserMoves)) : Winner

Equations

• One or more equations did not get rendered due to their size.
• treeCompArbGame leafCondition midCondition da (ABTree.leaf (some a)) chooser = if leafCondition h a da.res = true then Player.Proposer else Player.Chooser
• treeCompArbGame leafCondition midCondition da (ABTree.node (some proposition) nextProposerLeft nextProposerRight) chooser = Player.Proposer
• treeCompArbGame leafCondition midCondition da reveler✝ chooser = Player.Chooser

def tree_comp_winning_conditions {α α' β γ : Type} (leafCondition : α → α' → γ → Prop) (midCondition : β → γ → γ → γ → Prop) (da : CompTree α β γ) (player : ABTree (Option α') (Option (γ × γ))) : Prop

Equations

• One or more equations did not get rendered due to their size.
• tree_comp_winning_conditions leafCondition midCondition da (ABTree.leaf (some a)) = leafCondition h a da.res
• tree_comp_winning_conditions leafCondition midCondition da reveler✝ = False

def splitter_tree_game {α α' β β' γ γ' : Type} (splitter : γ → γ' → γ × γ) (leafCondition : α' → α → γ → Winner) (midCondition : β' → β → γ → γ → γ → Winner) (da : CompTree α' β' γ) (reveler : ABTree (Option α) (Option (β × γ'))) (chooser : ABTree Unit (γ × β × γ × γ → Option ChooserMoves)) : Winner

def reveler_winning_condition {α α' β γ : Type} (leafCondition : α → α' → γ → Bool) (midCondition : β → γ → γ → γ → Bool) (da : CompTree α β γ) (reveler : ABTree (Option α') (Option (γ × γ))) : Prop

Equations

• One or more equations did not get rendered due to their size.
• reveler_winning_condition leafCondition midCondition da (ABTree.leaf (some a')) = (leafCondition a a' da.res = true)
• reveler_winning_condition leafCondition midCondition da reveler✝ = False

def winning_condition_player {α α' β β' γ : Type} (leafCondition : α' → α → γ → Prop) (midCondition : β' → β → γ → Prop) (splitter : γ → β → γ × γ) (da : CompTree α' β' γ) (player : ABTree (Option α) (Option β)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• winning_condition_player leafCondition midCondition splitter da (ABTree.leaf (some a)) = leafCondition h a da.res
• winning_condition_player leafCondition midCondition splitter da reveler✝ = False

def gen_to_fun_chooser {α β γ : Type} [BEq β] : ABTree (Option α) (Option β) → ABTree Unit (γ → β → Option ChooserMoves)

Equations

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

theorem winning_proposer_wins {α α' β' γ : Type} (leafCondition : α' → α → γ → Bool) (midCondition : β' → γ → γ → γ → Bool) (da : CompTree α' β' γ) (reveler : ABTree (Option α) (Option (γ × γ))) (good_reveler : reveler_winning_condition leafCondition midCondition da reveler) (chooser : ABTree Unit (γ × γ × γ → Option ChooserMoves)) : treeCompArbGame leafCondition midCondition da reveler chooser = Player.Proposer

def prop_winner : Winner → Prop

Equations

• prop_winner Player.Proposer = True
• prop_winner Player.Chooser = False

theorem prop_win_chooser (p : Winner) : ¬prop_winner p ↔ p = Player.Chooser

axiom no_challenge_matching_data {α α' β β' γ : Type} {splitter : γ → β → γ × γ} {da : CompTree α' β' γ} {leafCondition : α' → α → γ → Prop} {midCondition : β' → β → γ → Prop} {player : ABTree (Option α) (Option β)} (knowing : winning_condition_player leafCondition midCondition splitter da player) {other_player : ABTree (Option α) (Option β)} : winning_condition_player leafCondition midCondition splitter da other_player

def Unique_Leaf_Condition2 {α α' γ : Type} (lc : α → α' → γ → Winner) : Prop

Equations

• Unique_Leaf_Condition2 lc = ∀ (a : α) (x y : α') (r r' : γ), ¬x = y → lc a x r = Player.Chooser → ¬lc a y r' = Player.Proposer

def top_elem {α β : Type} : ABTree α β → α ⊕ β

Equations

• top_elem = ABTree.getI' Sum.inl Sum.inr

def homogeneous_tree_game {pinfo γ : Type} (winning_condition : pinfo → γ → γ → γ → Winner) (da : ABTree pinfo pinfo) (rn : γ × γ) (reveler : ABTree (Option γ) (Option γ)) (chooser : ABTree Unit (pinfo × γ × γ × γ → Option ChooserMoves)) : Winner

Equations

• One or more equations did not get rendered due to their size.
• homogeneous_tree_game winning_condition (ABTree.leaf pub_now) rn (ABTree.leaf (some h)) chooser = winning_condition pub_now rn.1 h rn.2
• homogeneous_tree_game winning_condition (ABTree.node i bL bR) rn (ABTree.node none bL_1 bR_1) chooser = Player.Chooser
• homogeneous_tree_game winning_condition (ABTree.node i bL bR) rn (ABTree.leaf v) chooser = Player.Chooser
• homogeneous_tree_game winning_condition (ABTree.node i bL bR) rn (ABTree.node (some val) bL_1 bR_1) (ABTree.leaf v) = Player.Proposer
• homogeneous_tree_game winning_condition (ABTree.leaf v) rn reveler chooser = Player.Proposer

structure ImpTreePath (n : ℕ) (α γ : Type) : Type

• data : α × ISkeleton n
• res : γ

def ExpTree (n : ℕ) (α α' β : Type) : Type

Equations

• ExpTree n α α' β = ImpTreePath n α' (ABTree α β)

def pathToElem {α γ : Type} {n : ℕ} (leafCondition : ImpTreePath 0 α γ → Winner) (nodeCondition : γ × γ × γ → Winner) (da : ImpTreePath 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.
• pathToElem leafCondition nodeCondition da_2 proposer_2 chooser_2 = leafCondition da_2

def optJoin {α : Type} : Option (Option α) → Option α

Equations

• optJoin none = none
• optJoin (some none) = none
• optJoin (some (some j)) = some j

def skeleton_da_to_tree {lgn : ℕ} {γ : Type} (skeleton : ISkeleton (2 ^ lgn.succ - 1)) (res : γ) : CompTree SkElem SkElem γ

Equations

• skeleton_da_to_tree skeleton res = { data := perfectSeq skeleton, res := res }

def Unique_Leaf_Condition {α α' γ : Type} (lc : α → α' → γ → Bool) : Prop

Equations

• Unique_Leaf_Condition lc = ∀ (a : α) (x y : α') (r r' : γ), ¬r = r' → lc a x r = true → lc a y r' = false

def Unique_Mid_Condition {β γ : Type} (md : β → γ → γ → γ → Bool) : Prop

Equations

• Unique_Mid_Condition md = ∀ (b : β) (k1 k2 x y : γ), ¬k1 = k2 → ¬md b k1 x y = md b k2 x y

theorem chooser_data_availability {α α' β γ : Type} [BEq γ] [LawfulBEq γ] (leafCondition : α → α' → γ → Bool) (unique_leaf : Unique_Leaf_Condition leafCondition) (midCondition : β → γ → γ → γ → Bool) (unique_mid : Unique_Mid_Condition midCondition) (data : ABTree α β) (ch_res da_res : γ) (reveler : ABTree (Option α') (Option (γ × γ))) (wise_chooser : ABTree α' (γ × γ)) (win_chooser : tree_comp_winning_conditions (fun (x : α) (y : α') (z : γ) => leafCondition x y z = true) (fun (w : β) (x y z : γ) => midCondition w x y z = true) { data := data, res := ch_res } (ABTree.map some some wise_chooser)) (hneq : ¬ch_res = da_res) : treeCompArbGame leafCondition midCondition { data := data, res := da_res } reveler (ABTree.map (fun (x : α') => ()) (fun (k : γ × γ) (gargs : γ × γ × γ) => if (k.1 == gargs.2.1 && k.2 == gargs.2.2) = true then some ChooserPrimMoves.Now else if (k.1 != gargs.2.1) = true then some (ChooserPrimMoves.Continue Side.Left) else some (ChooserPrimMoves.Continue Side.Right)) wise_chooser) = Player.Chooser

def leaf_condition_length_one {ℍ : Type} [BEq ℍ] [HashMagma ℍ] : SkElem → ℍ → Range ℍ → Bool

Equations

• leaf_condition_length_one side prop (right_l, right_r) = (op_side side right_l prop == right_r)

def spl_game {ℍ : Type} [BEq ℍ] [m : HashMagma ℍ] (da : CompTree SkElem Unit (Range ℍ)) (proposer : ABTree (Option ℍ) (Option ℍ)) (chooser : ABTree Unit (Range ℍ → ℍ → Option ChooserMoves)) : Winner

Equations

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

def gen_chooser_opt {ℍ : Type} [BEq ℍ] (data : Option (ℍ × ℍ)) (proposed : ℍ × ℍ × ℍ) : Option ChooserMoves

Equations

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