OAI/Combinatorics/IndependentSets/Machines/Correct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.Expr.Correct line 10
  2. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_const line 15
  3. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_arg line 19
  4. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_length line 26
  5. theorem OAI.IndependentSetsCut.CounterMachine.Expr.binary_start line 31
  6. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_add line 48
  7. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_sub line 72
  8. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_zero line 96
  9. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_bit line 110
  10. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.assoc line 140
  11. theorem OAI.IndependentSetsCut.CounterMachine.Expr.correct_mul line 152