OAI/Combinatorics/IndependentSets/Machines/BitValue.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.Expr.bitValue line 10
  2. def OAI.IndependentSetsCut.CounterMachine.Expr.zeroPrefix line 12
  3. def OAI.IndependentSetsCut.CounterMachine.Expr.wordValue line 15
  4. def OAI.IndependentSetsCut.CounterMachine.Expr.prefixZeros line 18
  5. def OAI.IndependentSetsCut.CounterMachine.Expr.word line 19
  6. theorem OAI.IndependentSetsCut.CounterMachine.Expr.prefixZeros_eval line 22
  7. theorem OAI.IndependentSetsCut.CounterMachine.Expr.word_eval line 29
  8. theorem OAI.IndependentSetsCut.CounterMachine.Expr.bitValue_cons_zero line 34
  9. theorem OAI.IndependentSetsCut.CounterMachine.Expr.bitValue_cons_succ line 36
  10. theorem OAI.IndependentSetsCut.CounterMachine.Expr.zeroPrefix_zero line 38
  11. theorem OAI.IndependentSetsCut.CounterMachine.Expr.zeroPrefix_cons_succ line 39
  12. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_nil line 45
  13. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_true line 47
  14. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_false_zero line 52
  15. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_false_succ line 56
  16. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_block_zero line 61
  17. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_block_succ line 67
  18. def OAI.IndependentSetsCut.CounterMachine.Expr.unaryWords line 73
  19. theorem OAI.IndependentSetsCut.CounterMachine.Expr.wordValue_encoded line 75
  20. theorem OAI.IndependentSetsCut.CounterMachine.Expr.indicator_and line 90
  21. def OAI.IndependentSetsCut.CounterMachine.Expr.divides line 94
  22. theorem OAI.IndependentSetsCut.CounterMachine.Expr.divides_eval line 95
  23. def OAI.IndependentSetsCut.CounterMachine.Expr.prime line 99
  24. theorem OAI.IndependentSetsCut.CounterMachine.Expr.prime_eval line 102
  25. def OAI.IndependentSetsCut.CounterMachine.Expr.powTwo line 125
  26. theorem OAI.IndependentSetsCut.CounterMachine.Expr.powTwo_eval line 130
  27. def OAI.IndependentSetsCut.CounterMachine.Expr.size line 164
  28. theorem OAI.IndependentSetsCut.CounterMachine.Expr.count_powers line 166
  29. theorem OAI.IndependentSetsCut.CounterMachine.Expr.size_eval line 179
  30. def OAI.IndependentSetsCut.CounterMachine.Expr.digitPower line 184
  31. theorem OAI.IndependentSetsCut.CounterMachine.Expr.digitPower_eval line 188
  32. def OAI.IndependentSetsCut.CounterMachine.Expr.digit line 206
  33. theorem OAI.IndependentSetsCut.CounterMachine.Expr.digit_eval line 208