OAI/Computability/VertexCover/Machines/Lists.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Machine.listBits line 43
  2. theorem OAI.VertexCover.Machine.listBits_nil line 47
  3. theorem OAI.VertexCover.Machine.listBits_cons line 48
  4. theorem OAI.VertexCover.Machine.pairBits_length line 51
  5. theorem OAI.VertexCover.Machine.listBits_cons_length line 54
  6. theorem OAI.VertexCover.Machine.listBits_length_pos line 58
  7. theorem OAI.VertexCover.Machine.list_length_le_bits line 62
  8. theorem OAI.VertexCover.Machine.listBits_append_length line 68
  9. theorem OAI.VertexCover.Machine.listBits_reverse_length line 74
  10. def OAI.VertexCover.Machine.ListProject.trans line 86
  11. theorem OAI.VertexCover.Machine.ListProject.bound line 92
  12. theorem OAI.VertexCover.Machine.ListProject.normal line 98
  13. theorem OAI.VertexCover.Machine.ListProject.encoded line 105
  14. def OAI.VertexCover.Machine.Poly.listCons line 118
  15. def OAI.VertexCover.Machine.Poly.listTail line 122
  16. def OAI.VertexCover.Machine.Poly.listHeadD line 129
  17. def OAI.VertexCover.Machine.Poly.listHasHead line 136
  18. def OAI.VertexCover.Machine.Poly.swap line 140
  19. abbrev OAI.VertexCover.Machine.flagBits line 144
  20. def OAI.VertexCover.Machine.Poly.flag line 146
  21. def OAI.VertexCover.Machine.Poly.flagPair line 150
  22. def OAI.VertexCover.Machine.Fold.body line 158
  23. def OAI.VertexCover.Machine.Fold.bodyPoly line 162
  24. theorem OAI.VertexCover.Machine.Fold.run line 174
  25. def OAI.VertexCover.Machine.Poly.fold line 189