Project

Namespaces

Public Vars

latte-nats.times

The multiplication defined on ℕ.

*

(* [m nat] [n nat])
((times m) n)

Definition: The function that multiplies m with n.

mult-prop

(mult-prop [m nat])
(lambda
 [g (==> nat nat)]
 (and (= (g zero) zero) (forall [n nat] (= (g (succ n)) (+ m (g n))))))

Definition: The property of the multiplication of m to a natural integer.

mult-unique

(mult-unique [m nat])
(q/unique (mult-prop m))

Theorem: The unicity of the multiplication function, through mult-prop.

times

(times [m nat])
(q/the (mult-unique m))

Definition: The function that multiplies m to a natural number

times-assoc

(times-assoc [m nat] [n nat] [p nat])
(= (* (* m n) p) (* m (* n p)))

Theorem: Associativity of multiplication.

times-commute

(times-commute [m nat] [n nat])
(= (* m n) (* n m))

Theorem: Commutativity of multiplication.

times-dist-plus

(times-dist-plus [m nat] [n nat] [p nat])
(= (* m (+ n p)) (+ (* m n) (* m p)))

Theorem: Distributivity of multiplication over addition.

times-prop

(times-prop [m nat])
(and
 (= (* m zero) zero)
 (forall [n nat] (= (* m (succ n)) (+ m (* m n)))))

Theorem:

times-succ

(times-succ [m nat] [n nat])
(= (* m (succ n)) (+ m (* m n)))

Theorem:

times-succ-swap-both

(times-succ-swap-both [m nat] [n nat])
(= (* (succ n) m) (+ (* m n) m))

Theorem:

times-succ-swap-left

(times-succ-swap-left [n nat] [m nat])
(= (* (succ n) m) (+ m (* n m)))

Theorem:

times-succ-swap-right

(times-succ-swap-right [m nat] [n nat])
(= (* m (succ n)) (+ (* m n) m))

Theorem:

times-zero

(times-zero [n nat])
(= (* n zero) zero)

Theorem:

times-zero-swap

(times-zero-swap [n nat])
(= (* zero n) zero)

Theorem: