OAI/Computability/MinUncut/Games/HintSimulation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Outer.HintCoefficients line 13
  2. def OAI.MinUncut.Outer.secondHints line 16
  3. def OAI.MinUncut.Outer.firstHints line 19
  4. structure OAI.MinUncut.Outer.HintedStrategy line 23
  5. def OAI.MinUncut.Outer.hintedWins line 27
  6. def OAI.MinUncut.Outer.patch line 33
  7. lemma OAI.MinUncut.Outer.patch_active line 37
  8. lemma OAI.MinUncut.Outer.patch_inactive line 42
  9. lemma OAI.MinUncut.Outer.patch_comp line 47
  10. def OAI.MinUncut.Outer.slotZero line 53
  11. def OAI.MinUncut.Outer.readBit line 56
  12. lemma OAI.MinUncut.Outer.projection_hidden_bit line 60
  13. lemma OAI.MinUncut.Outer.firstHints_position_independent line 68
  14. lemma OAI.MinUncut.Outer.ordinary_accepts_of_valid_coordinate line 75
  15. lemma OAI.MinUncut.Outer.secondQuestion_patch line 85
  16. theorem OAI.MinUncut.Outer.active_simulation line 102