blob: 09d014d3a69ae8826dddbbb8003082e08e89c9d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
\begin{datatype}\label{propform}
%! infixr 0
Define $\propform$ inductively as follows.
\begin{enumerate}
\item $\propbot \in \propform$.
\item $\propvar{n} \in \propform$ for
$n \in \{\emptyset\}$.
\item $(p \propto q) \in \propform$ for $p \in \propform$ and $q \in \propform$.
\end{enumerate}
\end{datatype}
\begin{proposition}\label{propform_bot_test}
$\propbot \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propbot_intro}.
\end{proof}
\begin{proposition}\label{propform_var_test}
If $\emptyset \in \{\emptyset\}$, then
$\propvar{\emptyset} \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propvar_intro}.
\end{proof}
\begin{proposition}\label{propform_imp_test}
$(\propbot \propto \propbot) \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propbot_intro,propform_propto_intro}.
\end{proof}
\begin{proposition}\label{propform_distinct_test}
$\propbot \neq (\propbot \propto \propbot)$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propbot_propto_distinct}.
\end{proof}
\begin{proposition}\label{propform_injective_test}
If $\propvar{x} = \propvar{y}$, then $x = y$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propvar_injective}.
\end{proof}
|
