OAI/Combinatorics/ThinTrees/Arithmetic/UnaryArithmetic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Unary arithmetic.

  1. lemma OAI.CurrentKS.Realization.pred_iterate line 15
  2. instance OAI.CurrentKS.Realization.size_natPred line 20
  3. def OAI.CurrentKS.Realization.natSub line 27
  4. instance OAI.CurrentKS.Realization.poly_natSub line 30
  5. def OAI.CurrentKS.Realization.natDivBinary line 32
  6. instance OAI.CurrentKS.Realization.poly_natDivBinary line 38
  7. def OAI.CurrentKS.Realization.natDiv line 40
  8. instance OAI.CurrentKS.Realization.poly_natDiv line 42
  9. def OAI.CurrentKS.Realization.natMod line 55
  10. instance OAI.CurrentKS.Realization.poly_natMod line 62
  11. def OAI.CurrentKS.Realization.Realizes.nadd line 65
  12. def OAI.CurrentKS.Realization.Realizes.nmul line 67
  13. def OAI.CurrentKS.Realization.Realizes.nsub line 69
  14. def OAI.CurrentKS.Realization.Realizes.ndiv line 71
  15. def OAI.CurrentKS.Realization.Realizes.nmod line 73
  16. def OAI.CurrentKS.Realization.Realizes.neq line 75
  17. def OAI.CurrentKS.Realization.Realizes.nlt line 77
  18. instance OAI.CurrentKS.Realization.(instance at line 79) line 79
  19. instance OAI.CurrentKS.Realization.(instance at line 81) line 81
  20. instance OAI.CurrentKS.Realization.(instance at line 83) line 83
  21. instance OAI.CurrentKS.Realization.(instance at line 85) line 85
  22. instance OAI.CurrentKS.Realization.(instance at line 87) line 87
  23. instance OAI.CurrentKS.Realization.(instance at line 89) line 89
  24. instance OAI.CurrentKS.Realization.(instance at line 91) line 91