Precedes Next

From ProofWiki

Jump to: navigation, search

Theorem

Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup.

Then:

$\forall n \in S: n \prec n \circ 1$

Consequently:

$\forall n, p \in S: n \prec p \iff n \circ 1 \preceq p$

From Zero Precedes One, we have that $0 \prec 1$.

So:

$n = n \circ 0 \prec n \circ 1$

To show that $n \prec p \implies n \circ 1 \preceq p$:

$\displaystyle $	$\displaystyle $	$\displaystyle $	$\displaystyle n$	$\prec$	$\displaystyle p$	$\displaystyle $	$\displaystyle $	$\displaystyle $
$\displaystyle $	$\displaystyle \implies$	$\displaystyle $	$\displaystyle n \circ 0$	$\ne$	$\displaystyle p$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Definition of zero
$\displaystyle $	$\displaystyle \implies$	$\displaystyle $	$\displaystyle p \ominus n$	$\ne$	$\displaystyle 0$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Definition of minus
$\displaystyle $	$\displaystyle \implies$	$\displaystyle $	$\displaystyle p \ominus n$	$\notin$	$\displaystyle S^*$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Zero Complement
$\displaystyle $	$\displaystyle \implies$	$\displaystyle $	$\displaystyle 1$	$\preceq$	$\displaystyle p \ominus n$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Smallest Element of Zero Complement of Naturally Ordered Semigroup
$\displaystyle $	$\displaystyle \implies$	$\displaystyle $	$\displaystyle n \circ 1$	$\preceq$	$\displaystyle p$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Definition of minus

To show that $n \circ 1 \preceq p \implies n \prec p$:

$\blacksquare$

\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle n\)	\(\prec\)	\(\displaystyle p\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
\(\displaystyle \)	\(\displaystyle \implies\)	\(\displaystyle \)	\(\displaystyle n \circ 0\)	\(\ne\)	\(\displaystyle p\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Definition of zero
\(\displaystyle \)	\(\displaystyle \implies\)	\(\displaystyle \)	\(\displaystyle p \ominus n\)	\(\ne\)	\(\displaystyle 0\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Definition of minus
\(\displaystyle \)	\(\displaystyle \implies\)	\(\displaystyle \)	\(\displaystyle p \ominus n\)	\(\notin\)	\(\displaystyle S^*\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Zero Complement
\(\displaystyle \)	\(\displaystyle \implies\)	\(\displaystyle \)	\(\displaystyle 1\)	\(\preceq\)	\(\displaystyle p \ominus n\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Smallest Element of Zero Complement of Naturally Ordered Semigroup
\(\displaystyle \)	\(\displaystyle \implies\)	\(\displaystyle \)	\(\displaystyle n \circ 1\)	\(\preceq\)	\(\displaystyle p\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Definition of minus