OAI/Computability/MatchingCount/UnaryArithmetic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinaryMatching.StackCode.Poly.natSucc line 11
  2. theorem OAI.BinaryMatching.StackCode.Poly.natPred line 17
  3. theorem OAI.BinaryMatching.StackCode.Poly.natZeroTest line 22
  4. theorem OAI.BinaryMatching.StackCode.Poly.natAdd line 28
  5. theorem OAI.BinaryMatching.StackCode.Poly.natSub line 34
  6. theorem OAI.BinaryMatching.StackCode.Poly.boolNot line 43
  7. theorem OAI.BinaryMatching.StackCode.Poly.boolAnd line 47
  8. theorem OAI.BinaryMatching.StackCode.Poly.boolOr line 51
  9. theorem OAI.BinaryMatching.StackCode.Poly.natLE line 55
  10. theorem OAI.BinaryMatching.StackCode.Poly.natLT line 59
  11. theorem OAI.BinaryMatching.StackCode.Poly.natEQ line 64
  12. def OAI.BinaryMatching.StackCode.Poly.addStep line 70
  13. lemma OAI.BinaryMatching.StackCode.Poly.addStep_iterate line 71
  14. theorem OAI.BinaryMatching.StackCode.Poly.natMul line 76
  15. theorem OAI.BinaryMatching.StackCode.Poly.natMin line 88
  16. theorem OAI.BinaryMatching.StackCode.Poly.natMax line 92
  17. theorem OAI.BinaryMatching.StackCode.Poly.natLe_apply line 97
  18. theorem OAI.BinaryMatching.StackCode.Poly.natLt_apply line 99
  19. theorem OAI.BinaryMatching.StackCode.Poly.natEq_apply line 101
  20. theorem OAI.BinaryMatching.StackCode.Poly.natPow line 103