OAI/Combinatorics/IndependentSets/Encoding/BinaryEvents.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.LargeIndependentSets.BinarySyntax.Mark line 8
  2. def OAI.LargeIndependentSets.BinarySyntax.event line 13
  3. def OAI.LargeIndependentSets.BinarySyntax.shift line 18
  4. lemma OAI.LargeIndependentSets.BinarySyntax.shift_nil line 21
  5. lemma OAI.LargeIndependentSets.BinarySyntax.shift_cons line 22
  6. lemma OAI.LargeIndependentSets.BinarySyntax.shift_append line 24
  7. lemma OAI.LargeIndependentSets.BinarySyntax.shift_shift line 26
  8. lemma OAI.LargeIndependentSets.BinarySyntax.shift_zero line 28
  9. def OAI.LargeIndependentSets.BinarySyntax.events line 30
  10. lemma OAI.LargeIndependentSets.BinarySyntax.events_append line 34
  11. lemma OAI.LargeIndependentSets.BinarySyntax.events_header line 42
  12. lemma OAI.LargeIndependentSets.BinarySyntax.events_name line 47
  13. lemma OAI.LargeIndependentSets.BinarySyntax.events_literal line 52
  14. def OAI.LargeIndependentSets.BinarySyntax.clauseMark line 56
  15. lemma OAI.LargeIndependentSets.BinarySyntax.events_clause line 59
  16. lemma OAI.LargeIndependentSets.BinarySyntax.mem_shift line 95
  17. lemma OAI.LargeIndependentSets.BinarySyntax.events_complete line 102
  18. lemma OAI.LargeIndependentSets.BinarySyntax.event_clause_location line 129
  19. lemma OAI.LargeIndependentSets.BinarySyntax.events_bound line 148
  20. lemma OAI.LargeIndependentSets.BinarySyntax.clause_event_location line 163
  21. lemma OAI.LargeIndependentSets.BinarySyntax.event_formula_location line 175
  22. lemma OAI.LargeIndependentSets.BinarySyntax.formula_clause_event line 186