Sam Valentine

Written September 1999.

Last updated September 1999.

section numlaws parents numdefs, corelaws |

This section contains the CADi version of some laws about numbers in the mathematical toolkit of Z.

Those laws which depend solely on the definitions in the prelude are given in the file corelaws.z, which is a parent of this one.

We could here state and prove various useful theorems about `,
both because of their usefulness, and to assist in proving
the consistency of the definitions in numdefs.
`

The theorems would mainly be to the effect
that ` is an Abelian monoid under ``_ * _`,
and `_ * _` distributes through `_ + _`.

zeroTimesBEqZero ==

? b: 0 * b = 0 |

OneTimesBEqB ==

? b: 1 * b = b |

TimesCommutes ==

? a, b: a * b = b * a |

TimesDistributesThruPlus ==

? a, b, c: a * (b + c) = (a * b) + (a * c) |

TimesClosed ==

? a, b: a * b |

TimesAssociates ==

? a, b, c: (a * b) * c = a * (b * c) |

TimesConstInjective ==

? a, b: ; c: _{1} | a * c = b * c a = b |

IT 18-Feb-2000