OAI/Combinatorics/IndependentSets/Machines/FramedLen.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.Expr.framedLen line 10
  2. def OAI.IndependentSetsCut.CounterMachine.Expr.framedBit line 11
  3. theorem OAI.IndependentSetsCut.CounterMachine.Expr.framedLen_eval line 15
  4. theorem OAI.IndependentSetsCut.CounterMachine.Expr.framedBit_eval line 19
  5. def OAI.IndependentSetsCut.CounterMachine.frame line 36
  6. theorem OAI.IndependentSetsCut.CounterMachine.frame_length line 40
  7. theorem OAI.IndependentSetsCut.CounterMachine.frame_get line 45
  8. theorem OAI.IndependentSetsCut.CounterMachine.frame_bits_get line 60
  9. def OAI.IndependentSetsCut.CounterMachine.Expr.listSum line 81
  10. theorem OAI.IndependentSetsCut.CounterMachine.Expr.listSum_eval line 83
  11. def OAI.IndependentSetsCut.CounterMachine.Expr.finiteSum line 92
  12. theorem OAI.IndependentSetsCut.CounterMachine.Expr.finiteSum_eval line 94
  13. def OAI.IndependentSetsCut.CounterMachine.Expr.least line 99
  14. theorem OAI.IndependentSetsCut.CounterMachine.Expr.least_eval line 105
  15. theorem OAI.IndependentSetsCut.CounterMachine.Expr.least_eq line 134