OAI/Computability/MinUncut/Machines/MachineBinaryFormula.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.BinaryFormula.clauseNames line 11
  2. def OAI.MinUncutGames.BinaryFormula.sourceNames line 14
  3. def OAI.MinUncutGames.BinaryFormula.activeNames line 17
  4. theorem OAI.MinUncutGames.BinaryFormula.literal_mem_active line 20
  5. def OAI.MinUncutGames.BinaryFormula.compactIndex line 28
  6. def OAI.MinUncutGames.BinaryFormula.decodeName line 32
  7. def OAI.MinUncutGames.BinaryFormula.compactLiteral line 35
  8. def OAI.MinUncutGames.BinaryFormula.compactClause line 39
  9. def OAI.MinUncutGames.BinaryFormula.compactClauses line 45
  10. def OAI.MinUncutGames.BinaryFormula.dense line 48
  11. def OAI.MinUncutGames.BinaryFormula.restrictAssignment line 52
  12. def OAI.MinUncutGames.BinaryFormula.extendAssignment line 55
  13. theorem OAI.MinUncutGames.BinaryFormula.decode_compactIndex line 59
  14. theorem OAI.MinUncutGames.BinaryFormula.compactIndex_injective line 63
  15. theorem OAI.MinUncutGames.BinaryFormula.compactLiteral_positive line 69
  16. theorem OAI.MinUncutGames.BinaryFormula.eval_compact_restrict line 72
  17. theorem OAI.MinUncutGames.BinaryFormula.eval_compact_extend line 78
  18. def OAI.MinUncutGames.BinaryFormula.evaluationList line 88
  19. theorem OAI.MinUncutGames.BinaryFormula.evaluationList_restrict line 91
  20. theorem OAI.MinUncutGames.BinaryFormula.evaluationList_extend line 99
  21. def OAI.MinUncutGames.BinaryFormula.failedCount line 113
  22. theorem OAI.MinUncutGames.BinaryFormula.failedCount_restrict line 116
  23. theorem OAI.MinUncutGames.BinaryFormula.failedCount_extend line 120
  24. theorem OAI.MinUncutGames.BinaryFormula.clauseNames_flat_length line 124
  25. theorem OAI.MinUncutGames.BinaryFormula.dense_clause_count line 133
  26. theorem OAI.MinUncutGames.BinaryFormula.dense_variable_bound line 137
  27. theorem OAI.MinUncutGames.BinaryFormula.dense_completeness line 142
  28. theorem OAI.MinUncutGames.BinaryFormula.dense_reflects line 151
  29. theorem OAI.MinUncutGames.BinaryFormula.dense_satisfiable_iff line 161
  30. theorem OAI.MinUncutGames.BinaryFormula.dense_preserves_gap line 165
  31. theorem OAI.MinUncutGames.BinaryFormula.dense_encoding_bound line 172
  32. def OAI.MinUncutGames.BinaryEncoding.bitsValue line 197
  33. theorem OAI.MinUncutGames.BinaryEncoding.bitsValue_bits line 201
  34. def OAI.MinUncutGames.BinaryEncoding.parseFrame line 208
  35. theorem OAI.MinUncutGames.BinaryEncoding.parseFrame_encoded line 215
  36. theorem OAI.MinUncutGames.BinaryEncoding.frame_length line 221
  37. def OAI.MinUncutGames.BinaryEncoding.parseName line 227
  38. theorem OAI.MinUncutGames.BinaryEncoding.parseName_encoded line 232
  39. theorem OAI.MinUncutGames.BinaryEncoding.nameBits_length line 236
  40. theorem OAI.MinUncutGames.BinaryEncoding.nameBits_length_le_of_lt_pow line 240
  41. def OAI.MinUncutGames.BinaryEncoding.parseLiteral line 246
  42. theorem OAI.MinUncutGames.BinaryEncoding.parseLiteral_encoded line 252
  43. theorem OAI.MinUncutGames.BinaryEncoding.literalBits_length line 257
  44. def OAI.MinUncutGames.BinaryEncoding.parseClause line 261
  45. theorem OAI.MinUncutGames.BinaryEncoding.clause_three_entries line 267
  46. theorem OAI.MinUncutGames.BinaryEncoding.parseClause_encoded line 273
  47. def OAI.MinUncutGames.BinaryEncoding.clauseNameSize line 277
  48. theorem OAI.MinUncutGames.BinaryEncoding.clauseBits_length line 280
  49. def OAI.MinUncutGames.BinaryEncoding.namesBitSize line 285
  50. theorem OAI.MinUncutGames.BinaryEncoding.namesBitSize_nil line 288
  51. theorem OAI.MinUncutGames.BinaryEncoding.namesBitSize_cons line 290
  52. theorem OAI.MinUncutGames.BinaryEncoding.clausesBits_length line 294
  53. theorem OAI.MinUncutGames.BinaryEncoding.formulaBits_length line 303
  54. theorem OAI.MinUncutGames.BinaryEncoding.clauses_length_lt_bits line 308
  55. def OAI.MinUncutGames.BinaryEncoding.ordinarySize line 313
  56. theorem OAI.MinUncutGames.BinaryEncoding.ordinarySize_le_bits line 316
  57. theorem OAI.MinUncutGames.BinaryEncoding.bits_le_three_ordinarySize line 322
  58. def OAI.MinUncutGames.BinaryEncoding.parseClauses line 328
  59. theorem OAI.MinUncutGames.BinaryEncoding.parseClauses_encoded line 337
  60. def OAI.MinUncutGames.BinaryEncoding.decodeFormula line 352
  61. theorem OAI.MinUncutGames.BinaryEncoding.decodeFormula_encoded line 356
  62. theorem OAI.MinUncutGames.BinaryEncoding.formulaBits_injective line 365
  63. theorem OAI.MinUncutGames.BinaryEncoding.dense_encoding_bound line 370