OAI/Combinatorics/SharpRamsey/Trees/TreeDecoder.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.TreeDecoder.Domains line 12
  2. abbrev OAI.SharpLogRamsey.TreeDecoder.CapReader line 14
  3. def OAI.SharpLogRamsey.TreeDecoder.execute line 16
  4. lemma OAI.SharpLogRamsey.TreeDecoder.execute_height line 26
  5. lemma OAI.SharpLogRamsey.TreeDecoder.execute_numNodes line 38
  6. def OAI.SharpLogRamsey.TreeDecoder.flagDomain line 50
  7. def OAI.SharpLogRamsey.TreeDecoder.retained line 53
  8. lemma OAI.SharpLogRamsey.TreeDecoder.retained_sublist line 56
  9. lemma OAI.SharpLogRamsey.TreeDecoder.retained_mem line 60
  10. def OAI.SharpLogRamsey.TreeDecoder.output line 64
  11. def OAI.SharpLogRamsey.TreeDecoder.message line 73
  12. def OAI.SharpLogRamsey.TreeDecoder.decode line 82
  13. lemma OAI.SharpLogRamsey.TreeDecoder.forallâ‚‚_replicate_membership line 90
  14. theorem OAI.SharpLogRamsey.TreeDecoder.decoder_correct line 99
  15. def OAI.SharpLogRamsey.TreeDecoder.population line 116
  16. theorem OAI.SharpLogRamsey.TreeDecoder.output_sublist line 120