OAI/Combinatorics/IndependentSets/Machines/Represented.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.Expr.Represented line 11
  2. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.const line 16
  3. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.arg line 17
  4. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.word line 18
  5. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.add line 20
  6. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.sub line 22
  7. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.mul line 24
  8. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.div line 26
  9. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.mod line 28
  10. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.pow line 30
  11. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.eq line 32
  12. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.lt line 35
  13. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.cond line 38
  14. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.sum line 42
  15. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.finiteSum line 46
  16. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.rename line 50
  17. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.subst line 54
  18. theorem OAI.IndependentSetsCut.CounterMachine.Expr.Represented.congr line 58
  19. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.offset line 68
  20. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.words line 70
  21. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.offset_succ line 73
  22. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.offset_mono line 76
  23. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.words_succ line 82
  24. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.words_length line 86
  25. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.get_word line 91
  26. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.words_bit line 102
  27. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.indicator_exists line 134
  28. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.atIndex line 148
  29. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.closed line 149
  30. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.totalLength line 150
  31. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.startOffset line 152
  32. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.wordBit line 154
  33. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.atIndex_eval line 158
  34. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.closed_eval line 161
  35. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.totalLength_eval line 163
  36. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.startOffset_eval line 167
  37. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.wordBit_eval line 170
  38. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.table_eq_words line 178
  39. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.computer line 190
  40. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.computer_finiteAlphabet line 201
  41. def OAI.IndependentSetsCut.CounterMachine.UnaryTables.encodedComputer line 206
  42. lemma OAI.IndependentSetsCut.CounterMachine.UnaryTables.encodedComputer_finiteAlphabet line 217