|
456
|
1 |
% Chapter Template
|
|
|
2 |
|
|
|
3 |
\chapter{Common Identities In Simplification-Related Functions} % Main chapter title
|
|
|
4 |
|
|
|
5 |
\label{ChapterX} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}
|
|
|
6 |
|
|
|
7 |
|
|
|
8 |
|
|
|
9 |
%----------------------------------------------------------------------------------------
|
|
|
10 |
% SECTION 1
|
|
|
11 |
%----------------------------------------------------------------------------------------
|
|
|
12 |
|
|
|
13 |
\section{Idempotency of $\simp$}
|
|
|
14 |
|
|
|
15 |
\begin{equation}
|
|
|
16 |
\simp \;r = \simp\; \simp \; r
|
|
|
17 |
\end{equation}
|
|
|
18 |
This property means we do not have to repeatedly
|
|
|
19 |
apply simplification in each step, which justifies
|
|
|
20 |
our definition of $\blexersimp$.
|
|
|
21 |
It will also be useful in future proofs where properties such as
|
|
|
22 |
closed forms are needed.
|
|
|
23 |
The proof is by structural induction on $r$.
|
|
|
24 |
|
|
|
25 |
%-----------------------------------
|
|
|
26 |
% SUBSECTION 1
|
|
|
27 |
%-----------------------------------
|
|
|
28 |
\subsection{Syntactic Equivalence Under $\simp$}
|
|
|
29 |
We prove that minor differences can be annhilated
|
|
|
30 |
by $\simp$.
|
|
|
31 |
For example,
|
|
|
32 |
\begin{center}
|
|
|
33 |
$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
|
|
|
34 |
\simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
|
|
|
35 |
\end{center}
|
|
|
36 |
|
|
|
37 |
|
|
|
38 |
%-----------------------------------
|
|
|
39 |
% SUBSECTION 2
|
|
|
40 |
%-----------------------------------
|
|
|
41 |
|
|
|
42 |
\subsection{Subsection 2}
|
|
|
43 |
Morbi rutrum odio eget arcu adipiscing sodales. Aenean et purus a est pulvinar pellentesque. Cras in elit neque, quis varius elit. Phasellus fringilla, nibh eu tempus venenatis, dolor elit posuere quam, quis adipiscing urna leo nec orci. Sed nec nulla auctor odio aliquet consequat. Ut nec nulla in ante ullamcorper aliquam at sed dolor. Phasellus fermentum magna in augue gravida cursus. Cras sed pretium lorem. Pellentesque eget ornare odio. Proin accumsan, massa viverra cursus pharetra, ipsum nisi lobortis velit, a malesuada dolor lorem eu neque.
|
|
|
44 |
|
|
|
45 |
%----------------------------------------------------------------------------------------
|
|
|
46 |
% SECTION 2
|
|
|
47 |
%----------------------------------------------------------------------------------------
|
|
|
48 |
|
|
|
49 |
\section{Main Section 2}
|
|
|
50 |
|
|
|
51 |
Sed ullamcorper quam eu nisl interdum at interdum enim egestas. Aliquam placerat justo sed lectus lobortis ut porta nisl porttitor. Vestibulum mi dolor, lacinia molestie gravida at, tempus vitae ligula. Donec eget quam sapien, in viverra eros. Donec pellentesque justo a massa fringilla non vestibulum metus vestibulum. Vestibulum in orci quis felis tempor lacinia. Vivamus ornare ultrices facilisis. Ut hendrerit volutpat vulputate. Morbi condimentum venenatis augue, id porta ipsum vulputate in. Curabitur luctus tempus justo. Vestibulum risus lectus, adipiscing nec condimentum quis, condimentum nec nisl. Aliquam dictum sagittis velit sed iaculis. Morbi tristique augue sit amet nulla pulvinar id facilisis ligula mollis. Nam elit libero, tincidunt ut aliquam at, molestie in quam. Aenean rhoncus vehicula hendrerit.
|