OAI/Computability/VertexCover/Machines/Cardinal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Machine.firstName line 46
  2. def OAI.VertexCover.Machine.firstNamePoly line 48
  3. def OAI.VertexCover.Machine.boundedFirstNamePoly line 51
  4. theorem OAI.VertexCover.Machine.firstName_encoded line 57
  5. theorem OAI.VertexCover.Machine.names_length line 60
  6. theorem OAI.VertexCover.Machine.firstName_graph line 67
  7. theorem OAI.VertexCover.Machine.graph_card_le_bits line 71
  8. def OAI.VertexCover.Machine.Poly.graphCard line 77
  9. theorem OAI.VertexCover.Machine.firstName_list line 81
  10. theorem OAI.VertexCover.Machine.natList_length_le_bits line 84
  11. def OAI.VertexCover.Machine.Poly.natListCard line 87
  12. def OAI.VertexCover.Machine.Poly.natLT line 91