Project

Namespaces

Public Vars

latte-integers.plus

The addition defined on ℤ.

+

(+ [m int] [n int])
((plus m) n)

Definition: The function that adds m to n.

add-prop

(add-prop [m int])
(lambda
 [g (==> int int)]
 (and (= (g zero) m) (forall [x int] (= (g (succ x)) (succ (g x))))))

Definition: The property of the addition function on integers.

add-unique

(add-unique [m int])
(q/unique (add-prop m))

Theorem: The unicity of the addition function, through add-prop.

negative-plus

(negative-plus [n int] [m int])
(==> (negative n) (negative m) (negative (+ n m)))

Theorem:

negative-pos-plus

(negative-pos-plus)
(forall
 [n int]
 (==>
  (nat/negative n)
  (exists [m int] (and (positive m) (= (+ n m) zero)))))

Theorem:

negative-pos-plus-conv

(negative-pos-plus-conv)
(forall
 [n int]
 (==>
  (exists [m int] (and (positive m) (= (+ n m) zero)))
  (negative n)))

Theorem:

negative-pos-plus-equiv

(negative-pos-plus-equiv [n int])
(<=> (exists [m int] (and (positive m) (= (+ n m) zero))) (negative n))

Theorem:

plus

(plus [m int])
(q/the (add-unique m))

Definition: The function that adds m to an integer

plus-assoc

(plus-assoc [n int] [m int] [p int])
(= (+ n (+ m p)) (+ (+ n m) p))

Theorem:

plus-assoc-sym

(plus-assoc-sym [n int] [m int] [p int])
(= (+ (+ n m) p) (+ n (+ m p)))

Theorem:

plus-commute

(plus-commute [n int] [m int])
(= (+ n m) (+ m n))

Theorem:

plus-left-cancel

(plus-left-cancel [n int] [m int] [p int])
(==> (= (+ p n) (+ p m)) (= n m))

Theorem:

plus-left-cancel-conv

(plus-left-cancel-conv [n int] [m int] [p int])
(==> (= n m) (= (+ p n) (+ p m)))

Theorem:

plus-nat-closed

(plus-nat-closed)
(forall-in [n nat] (forall-in [m nat] (elem (+ n m) nat)))

Theorem: The addition is closed for natural integers.

plus-one

(plus-one [n int])
(= (+ n one) (succ n))

Theorem:

plus-pred

(plus-pred [m int] [n int])
(= (+ m (pred n)) (pred (+ m n)))

Theorem:

plus-pred-succ

(plus-pred-succ [n int] [m int])
(= (+ (pred n) (succ m)) (+ n m))

Theorem:

plus-pred-swap

(plus-pred-swap [m int] [n int])
(= (+ (pred m) n) (pred (+ m n)))

Theorem:

plus-pred-sym

(plus-pred-sym [m int] [n int])
(= (pred (+ m n)) (+ m (pred n)))

Theorem:

plus-prop

(plus-prop [m int])
(and
 (= ((plus m) zero) m)
 (forall [n int] (= ((plus m) (succ n)) (succ ((plus m) n)))))

Theorem:

plus-right-cancel

(plus-right-cancel [n int] [m int] [p int])
(==> (= (+ n p) (+ m p)) (= n m))

Theorem:

plus-right-cancel-conv

(plus-right-cancel-conv [n int] [m int] [p int])
(==> (= n m) (= (+ n p) (+ m p)))

Theorem:

plus-succ

(plus-succ [m int] [n int])
(= (+ m (succ n)) (succ (+ m n)))

Theorem:

plus-succ-pred

(plus-succ-pred [n int] [m int])
(= (+ (succ n) (pred m)) (+ n m))

Theorem:

plus-succ-swap

(plus-succ-swap [m int] [n int])
(= (+ (succ m) n) (succ (+ m n)))

Theorem:

plus-succ-sym

(plus-succ-sym [m int] [n int])
(= (succ (+ m n)) (+ m (succ n)))

Theorem:

plus-zero

(plus-zero [m int])
(= (+ m zero) m)

Theorem:

plus-zero-swap

(plus-zero-swap [m int])
(= (+ zero m) m)

Theorem:

positive-plus

(positive-plus)
(forall [n m int] (==> (positive n) (positive m) (positive (+ n m))))

Theorem: