25 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} |
25 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} |
26 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} |
26 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} |
27 \def\lparr{\mathopen{(\mkern-4mu\mid}} |
27 \def\lparr{\mathopen{(\mkern-4mu\mid}} |
28 \def\rparr{\mathclose{\mid\mkern-4mu)}} |
28 \def\rparr{\mathclose{\mid\mkern-4mu)}} |
29 |
29 |
30 \def\unk{{?}} |
30 %\def\unk{{?}} |
|
31 \def\unk{{\_}} |
31 \def\unkef{(\lambda x.\; \unk)} |
32 \def\unkef{(\lambda x.\; \unk)} |
32 \def\undef{(\lambda x.\; \_)} |
33 \def\undef{(\lambda x.\; \_)} |
33 %\def\unr{\textit{others}} |
34 %\def\unr{\textit{others}} |
34 \def\unr{\ldots} |
35 \def\unr{\ldots} |
35 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} |
36 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} |
929 \slshape Nitpick found a counterexample: |
930 \slshape Nitpick found a counterexample: |
930 \\[2\smallskipamount] |
931 \\[2\smallskipamount] |
931 \hbox{}\qquad Free variable: \nopagebreak \\ |
932 \hbox{}\qquad Free variable: \nopagebreak \\ |
932 \hbox{}\qquad\qquad $n = 1$ \\ |
933 \hbox{}\qquad\qquad $n = 1$ \\ |
933 \hbox{}\qquad Constants: \nopagebreak \\ |
934 \hbox{}\qquad Constants: \nopagebreak \\ |
934 \hbox{}\qquad\qquad $\textit{even} = (λx. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\ |
935 \hbox{}\qquad\qquad $\textit{even} = \unkef(0 := True, 1 := False, 2 := True, 3 := False)$ \\ |
935 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\ |
936 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\ |
936 \hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\ |
937 \hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\ |
937 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\ |
938 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\ |
938 \hbox{}\qquad\qquad\quad $( |
939 \hbox{}\qquad\qquad\quad $( |
939 \!\begin{aligned}[t] |
940 \!\begin{aligned}[t] |