Finite ranges of integers

From Automated Assistance for Formal Reasoning

Jump to: navigation, search

Assert for any $x,y \in \N$ , if $x < y$ then $\{x,\ldots,y\}$ is the set of integers from $x$ to $y$ and $\max \{x,\ldots,y\} = y$ .

Assert for any $x,y \in \N$ , if $x > y$ then $\{x,\ldots,y\} = \emptyset$ .

Assert for any $x, y, z$ , if $x$ is the set of integers from $y$ to $z$ then $max(x) = z$ .

Assert for any $x,y,z \in \N$ , if $y \geq x$ and $z \geq y+1$ then

$\{x,...,y\} \cup \{y+1,...,z\} = \{x,...,z\}$ .

Retrieved from "http://www.safre.org/wiki/index.php?title=Finite_ranges_of_integers"

Views

Personal tools

Search

Toolbox