latte-nats.plus
The addition defined on ℕ.
+
(+ [m nat] [n nat])((plus m) n)
Definition: The function that adds m to n.
add-prop
(add-prop [m nat])(lambda
[g (==> nat nat)]
(and (= (g zero) m) (forall [n nat] (= (g (succ n)) (succ (g n))))))
Definition: The property of the addition of m to a natural integer.
add-unique
(add-unique [m nat])(q/unique (add-prop m))
Theorem: The unicity of the addition function, through add-prop.
associative-plus
(associative-plus)(alg/associative +)
Theorem:
cancel-left-plus
(cancel-left-plus)(alg/cancel-left +)
Theorem:
cancel-right-plus
(cancel-right-plus)(alg/cancel-right +)
Theorem:
commutative-plus
(commutative-plus)(alg/commutative +)
Theorem:
identity-left-plus
(identity-left-plus)(alg/identity-left + zero)
Theorem:
identity-plus
(identity-plus)(alg/identity + zero)
Theorem:
identity-right-plus
(identity-right-plus)(alg/identity-right + zero)
Theorem:
monoid-plus
(monoid-plus)(alg/monoid + zero)
Theorem:
plus
(plus [m nat])(q/the (add-unique m))
Definition: The function that adds m to a natural integer
plus-any-zero-left
(plus-any-zero-left [m nat] [n nat])(==> (= (+ m n) zero) (= m zero))
Theorem:
plus-any-zero-right
(plus-any-zero-right [m nat] [n nat])(==> (= (+ m n) zero) (= n zero))
Theorem:
plus-assoc
(plus-assoc [m nat] [n nat] [p nat])(= (+ m (+ n p)) (+ (+ m n) p))
Theorem:
plus-comm-assoc
(plus-comm-assoc [m nat] [n nat] [p nat])(= (+ (+ m n) p) (+ (+ m p) n))
Theorem:
plus-commute
(plus-commute [m nat] [n nat])(= (+ m n) (+ n m))
Theorem:
plus-left-cancel
(plus-left-cancel [m nat] [n nat] [p nat])(==> (= (+ m n) (+ m p)) (= n p))
Theorem:
plus-left-cancel-conv
(plus-left-cancel-conv [m nat] [n nat] [p nat])(==> (= m n) (= (+ p m) (+ p n)))
Theorem:
plus-prop
(plus-prop [m nat])(and
(= ((plus m) zero) m)
(forall [n nat] (= ((plus m) (succ n)) (succ ((plus m) n)))))
Theorem:
plus-refl-zero
(plus-refl-zero [n nat] [k nat])(==> (= (+ n k) n) (= k zero))
Theorem:
plus-right-cancel
(plus-right-cancel [m nat] [n nat] [p nat])(==> (= (+ m p) (+ n p)) (= m n))
Theorem:
plus-right-cancel-conv
(plus-right-cancel-conv [m nat] [n nat] [p nat])(==> (= m n) (= (+ m p) (+ n p)))
Theorem:
plus-succ
(plus-succ [m nat] [n nat])(= (+ m (succ n)) (succ (+ m n)))
Theorem:
plus-succ-swap
(plus-succ-swap [m nat] [n nat])(= (+ (succ m) n) (succ (+ m n)))
Theorem:
plus-succ-sym
(plus-succ-sym [m nat] [n nat])(= (succ (+ m n)) (+ m (succ n)))
Theorem:
plus-zero
(plus-zero [m nat])(= (+ m zero) m)
Theorem:
plus-zero-swap
(plus-zero-swap [m nat])(= (+ zero m) m)
Theorem:
unique-identity-plus
(unique-identity-plus)(q/unique (alg/identity-def nat +))
Theorem: