OAI/Probability/ThorpShuffle/Reachability.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Thorp.Reachability.run_append line 15
  2. def OAI.Thorp.Reachability.zeroCoins line 26
  3. theorem OAI.Thorp.Reachability.step_false line 28
  4. theorem OAI.Thorp.Reachability.run_false line 34
  5. def OAI.Thorp.Reachability.returnMonoid line 43
  6. def OAI.Thorp.Reachability.returnGroup line 50
  7. theorem OAI.Thorp.Reachability.mem_returnGroup line 53
  8. theorem OAI.Thorp.Reachability.rotate_inv_pow line 58
  9. theorem OAI.Thorp.Reachability.inverse_conj_mem line 63
  10. theorem OAI.Thorp.Reachability.inverse_conj_pow_mem line 74
  11. theorem OAI.Thorp.Reachability.canceled_step_mem line 82
  12. theorem OAI.Thorp.Reachability.first_pair_swap line 95
  13. theorem OAI.Thorp.Reachability.first_pair_mem line 117
  14. theorem OAI.Thorp.Reachability.first_edge_mem line 123
  15. theorem OAI.Thorp.Reachability.rotate_pow_apply line 134
  16. theorem OAI.Thorp.Reachability.finRotate_pow_zero line 144
  17. theorem OAI.Thorp.Reachability.edge_swap_mem line 149
  18. theorem OAI.Thorp.Reachability.cube_connected line 165
  19. theorem OAI.Thorp.Reachability.all_swap_mem line 187
  20. theorem OAI.Thorp.Reachability.returnGroup_eq_top line 205
  21. theorem OAI.Thorp.Reachability.attainable_return line 213