OAI/Combinatorics/VariableWL/PrefixGame.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.PrefixParts.Data.Live line 12
  2. def OAI.VariableWL.PrefixParts.Data.observation line 17
  3. theorem OAI.VariableWL.PrefixParts.Data.live_of_sort line 22
  4. theorem OAI.VariableWL.PrefixParts.Data.observation_adj line 32
  5. theorem OAI.VariableWL.PrefixParts.Wiring.within_adj line 81
  6. abbrev OAI.VariableWL.PrefixParts.Data.LiveVertex line 110
  7. def OAI.VariableWL.PrefixParts.Data.liveGraph line 111
  8. def OAI.VariableWL.PrefixParts.Data.liveSpine line 114
  9. def OAI.VariableWL.PrefixParts.Data.liveTree line 117
  10. theorem OAI.VariableWL.PrefixParts.Data.live_tree_to_leaf line 120
  11. theorem OAI.VariableWL.PrefixParts.Data.live_spine_to_zero line 138
  12. theorem OAI.VariableWL.PrefixParts.Data.live_to_root line 148
  13. theorem OAI.VariableWL.PrefixParts.Data.zero_legal line 156
  14. def OAI.VariableWL.PrefixParts.Data.zeroValuation line 160
  15. def OAI.VariableWL.PrefixParts.Wiring.Live line 169
  16. def OAI.VariableWL.PrefixParts.Wiring.observation line 172
  17. theorem OAI.VariableWL.PrefixParts.Wiring.live_of_color line 176
  18. theorem OAI.VariableWL.PrefixParts.Wiring.root_observation line 187
  19. theorem OAI.VariableWL.PrefixParts.Wiring.observation_adj line 198
  20. abbrev OAI.VariableWL.PrefixParts.Wiring.LiveVertex line 222
  21. def OAI.VariableWL.PrefixParts.Wiring.liveGraph line 223
  22. def OAI.VariableWL.PrefixParts.Wiring.livePartHom line 226
  23. theorem OAI.VariableWL.PrefixParts.Wiring.word_of_live_reachable line 238
  24. theorem OAI.VariableWL.PrefixParts.Wiring.observation_sortWalk line 254
  25. def OAI.VariableWL.PrefixParts.Wiring.rootOfValuation line 270
  26. theorem OAI.VariableWL.PrefixParts.Wiring.zero_root_bits line 274
  27. def OAI.VariableWL.PrefixParts.Wiring.queryOwner line 281
  28. def OAI.VariableWL.PrefixParts.Wiring.selection line 284
  29. theorem OAI.VariableWL.PrefixParts.Wiring.selection_self line 290
  30. theorem OAI.VariableWL.PrefixParts.Wiring.selection_mate line 294
  31. theorem OAI.VariableWL.PrefixParts.Wiring.zero_queries_reachable line 298
  32. theorem OAI.VariableWL.PrefixParts.Wiring.readout_word line 331
  33. def OAI.VariableWL.PrefixParts.Wiring.query line 348
  34. abbrev OAI.VariableWL.PrefixParts.Wiring.Response line 351
  35. def OAI.VariableWL.PrefixParts.Wiring.response line 353
  36. theorem OAI.VariableWL.PrefixParts.Wiring.queryOwner_recognized line 357
  37. theorem OAI.VariableWL.PrefixParts.Wiring.winning_query_recognized line 372
  38. theorem OAI.VariableWL.PrefixParts.Wiring.winning_readout line 382