OAI/Combinatorics/IndependentSets/Machines/Printer.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.printer line 10
  2. def OAI.IndependentSetsCut.CounterMachine.printerTime line 12
  3. theorem OAI.IndependentSetsCut.CounterMachine.printer_evaluates line 17
  4. theorem OAI.IndependentSetsCut.CounterMachine.halted_eq line 31
  5. def OAI.IndependentSetsCut.CounterMachine.tableComputer line 40
  6. theorem OAI.IndependentSetsCut.CounterMachine.tableComputer_finiteAlphabet line 80
  7. def OAI.IndependentSetsCut.CounterMachine.Expr.rename line 89
  8. theorem OAI.IndependentSetsCut.CounterMachine.Expr.rename_eval line 100
  9. def OAI.IndependentSetsCut.CounterMachine.Expr.bindExpr line 111
  10. def OAI.IndependentSetsCut.CounterMachine.Expr.subst line 115
  11. theorem OAI.IndependentSetsCut.CounterMachine.Expr.subst_eval line 126
  12. def OAI.IndependentSetsCut.CounterMachine.Expr.positive line 139
  13. def OAI.IndependentSetsCut.CounterMachine.Expr.equal line 140
  14. def OAI.IndependentSetsCut.CounterMachine.Expr.le line 141
  15. def OAI.IndependentSetsCut.CounterMachine.Expr.lt line 142
  16. theorem OAI.IndependentSetsCut.CounterMachine.Expr.positive_eval line 144
  17. theorem OAI.IndependentSetsCut.CounterMachine.Expr.equal_eval line 148
  18. theorem OAI.IndependentSetsCut.CounterMachine.Expr.le_eval line 155
  19. theorem OAI.IndependentSetsCut.CounterMachine.Expr.lt_eval line 159
  20. def OAI.IndependentSetsCut.CounterMachine.Expr.cond line 163
  21. theorem OAI.IndependentSetsCut.CounterMachine.Expr.cond_eval line 164
  22. def OAI.IndependentSetsCut.CounterMachine.Expr.quotient line 168
  23. theorem OAI.IndependentSetsCut.CounterMachine.Expr.quotient_sum line 171
  24. theorem OAI.IndependentSetsCut.CounterMachine.Expr.quotient_eval line 182
  25. def OAI.IndependentSetsCut.CounterMachine.Expr.remainder line 190
  26. theorem OAI.IndependentSetsCut.CounterMachine.Expr.remainder_eval line 191
  27. def OAI.IndependentSetsCut.CounterMachine.Expr.power line 196
  28. theorem OAI.IndependentSetsCut.CounterMachine.Expr.power_eval line 199