OAI/Computability/PerfectCompleteness/Foundations/NormalizationLemmas.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.Normalization.tripleClause line 20
  2. def OAI.PerfectCompleteness.Normalization.normalizedTriple line 23
  3. def OAI.PerfectCompleteness.Normalization.outputVariables line 34
  4. def OAI.PerfectCompleteness.Normalization.oldVariable line 36
  5. def OAI.PerfectCompleteness.Normalization.freshVariable line 39
  6. def OAI.PerfectCompleteness.Normalization.copyVariable line 47
  7. def OAI.PerfectCompleteness.Normalization.paddingVariable line 51
  8. theorem OAI.PerfectCompleteness.Normalization.freshVariable_injective line 54
  9. theorem OAI.PerfectCompleteness.Normalization.copy_ne_copy line 65
  10. theorem OAI.PerfectCompleteness.Normalization.copy_ne_old line 74
  11. theorem OAI.PerfectCompleteness.Normalization.copy_ne_padding line 82
  12. theorem OAI.PerfectCompleteness.Normalization.old_ne_padding line 90
  13. def OAI.PerfectCompleteness.Normalization.mainClause line 98
  14. def OAI.PerfectCompleteness.Normalization.equalityClauses line 106
  15. def OAI.PerfectCompleteness.Normalization.gadget line 119
  16. def OAI.PerfectCompleteness.Normalization.gadgetClauses line 124
  17. theorem OAI.PerfectCompleteness.Normalization.equalityClauses_length line 128
  18. theorem OAI.PerfectCompleteness.Normalization.gadget_length line 131
  19. theorem OAI.PerfectCompleteness.Normalization.gadgetClauses_length line 134
  20. def OAI.PerfectCompleteness.Normalization.restrictAssignment line 137
  21. def OAI.PerfectCompleteness.Normalization.extendAssignment line 140
  22. theorem OAI.PerfectCompleteness.Normalization.extend_oldVariable line 152
  23. theorem OAI.PerfectCompleteness.Normalization.extend_copyVariable line 156
  24. theorem OAI.PerfectCompleteness.Normalization.restrict_extend line 165
  25. theorem OAI.PerfectCompleteness.Normalization.main_eval_of_copies_match line 170
  26. theorem OAI.PerfectCompleteness.Normalization.equalityClauses_failures line 178
  27. theorem OAI.PerfectCompleteness.Normalization.gadget_failures line 191
  28. theorem OAI.PerfectCompleteness.Normalization.clauseFailures_zero_iff line 206
  29. theorem OAI.PerfectCompleteness.Normalization.gadget_complete_of_copies_match line 211
  30. theorem OAI.PerfectCompleteness.Normalization.gadget_failure_domination line 221
  31. theorem OAI.PerfectCompleteness.Normalization.gadget_failed line 252
  32. def OAI.PerfectCompleteness.Normalization.normalizedClauses line 258
  33. def OAI.PerfectCompleteness.Normalization.normalize line 261
  34. theorem OAI.PerfectCompleteness.Normalization.normalize_clauses_eq_map line 265
  35. theorem OAI.PerfectCompleteness.Normalization.normalize_distinct line 270
  36. theorem OAI.PerfectCompleteness.Normalization.normalize_variables line 278
  37. theorem OAI.PerfectCompleteness.Normalization.normalize_clause_count line 281
  38. theorem OAI.PerfectCompleteness.Normalization.normalize_nonempty line 288
  39. theorem OAI.PerfectCompleteness.Normalization.normalize_completeness line 296
  40. theorem OAI.PerfectCompleteness.Normalization.failedCount_domination line 308
  41. theorem OAI.PerfectCompleteness.Normalization.normalize_reflects line 319
  42. theorem OAI.PerfectCompleteness.Normalization.normalize_satisfiable_iff line 330
  43. theorem OAI.PerfectCompleteness.Normalization.normalize_gap line 334
  44. abbrev OAI.PerfectCompleteness.NormalizationWords.Signs line 358
  45. abbrev OAI.PerfectCompleteness.NormalizationWords.Names line 359
  46. inductive OAI.PerfectCompleteness.NormalizationWords.NameRef line 361
  47. inductive OAI.PerfectCompleteness.NormalizationWords.SignRef line 366
  48. structure OAI.PerfectCompleteness.NormalizationWords.LiteralRecipe line 371
  49. def OAI.PerfectCompleteness.NormalizationWords.sourceValue line 376
  50. def OAI.PerfectCompleteness.NormalizationWords.offset line 380
  51. def OAI.PerfectCompleteness.NormalizationWords.nameValue line 384
  52. def OAI.PerfectCompleteness.NormalizationWords.signValue line 387
  53. def OAI.PerfectCompleteness.NormalizationWords.literalWords line 391
  54. def OAI.PerfectCompleteness.NormalizationWords.literalBits line 395
  55. def OAI.PerfectCompleteness.NormalizationWords.mainRecipe line 399
  56. def OAI.PerfectCompleteness.NormalizationWords.equalityRecipe line 402
  57. def OAI.PerfectCompleteness.NormalizationWords.recipe line 408
  58. theorem OAI.PerfectCompleteness.NormalizationWords.recipe_length line 411
  59. def OAI.PerfectCompleteness.NormalizationWords.words line 413
  60. def OAI.PerfectCompleteness.NormalizationWords.bits line 416
  61. def OAI.PerfectCompleteness.NormalizationWords.clauseSigns line 419
  62. def OAI.PerfectCompleteness.NormalizationWords.clauseNames line 421
  63. theorem OAI.PerfectCompleteness.NormalizationWords.encodeWords_flatMap line 423
  64. theorem OAI.PerfectCompleteness.NormalizationWords.bits_eq_flatMap line 429
  65. theorem OAI.PerfectCompleteness.NormalizationWords.gadget_words line 433
  66. theorem OAI.PerfectCompleteness.NormalizationWords.gadget_bits line 445
  67. def OAI.PerfectCompleteness.NormalizationWords.body line 452
  68. theorem OAI.PerfectCompleteness.NormalizationWords.encoded_body line 457
  69. theorem OAI.PerfectCompleteness.NormalizationWords.encoded_normalize line 465
  70. def OAI.PerfectCompleteness.NormalizationStream.blocks line 483
  71. theorem OAI.PerfectCompleteness.NormalizationStream.blocks_eq_finRange line 488
  72. theorem OAI.PerfectCompleteness.NormalizationStream.body_eq_blocks line 503
  73. theorem OAI.PerfectCompleteness.NormalizationStream.encoded_normalize line 508
  74. theorem OAI.PerfectCompleteness.NormalizationStream.blocks_length_le line 514