equal
deleted
inserted
replaced
57 \isamarkuptrue% |
57 \isamarkuptrue% |
58 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline |
58 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline |
59 \isamarkupfalse% |
59 \isamarkupfalse% |
60 \isamarkupfalse% |
60 \isamarkupfalse% |
61 \isanewline |
61 \isanewline |
62 \isanewline |
|
63 \isamarkupfalse% |
62 \isamarkupfalse% |
64 \isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse% |
63 \isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse% |
65 % |
64 % |
66 \begin{isamarkuptext}% |
65 \begin{isamarkuptext}% |
67 this is what we get: |
66 this is what we get: |
129 \isamarkupfalse% |
128 \isamarkupfalse% |
130 \isamarkuptrue% |
129 \isamarkuptrue% |
131 \isamarkupfalse% |
130 \isamarkupfalse% |
132 \isamarkuptrue% |
131 \isamarkuptrue% |
133 \isamarkupfalse% |
132 \isamarkupfalse% |
134 \isanewline |
|
135 \isanewline |
133 \isanewline |
136 \isanewline |
134 \isanewline |
137 \isanewline |
135 \isanewline |
138 \isamarkupfalse% |
136 \isamarkupfalse% |
139 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline |
137 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline |
194 \isamarkupfalse% |
192 \isamarkupfalse% |
195 \isamarkupfalse% |
193 \isamarkupfalse% |
196 \isamarkupfalse% |
194 \isamarkupfalse% |
197 \isamarkupfalse% |
195 \isamarkupfalse% |
198 \isanewline |
196 \isanewline |
199 \isanewline |
|
200 \isamarkupfalse% |
197 \isamarkupfalse% |
201 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline |
198 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline |
202 \isamarkupfalse% |
199 \isamarkupfalse% |
203 \isamarkupfalse% |
200 \isamarkupfalse% |
204 \isamarkupfalse% |
201 \isamarkupfalse% |
205 \isamarkupfalse% |
202 \isamarkupfalse% |
206 \isanewline |
|
207 \isanewline |
203 \isanewline |
208 \isanewline |
204 \isanewline |
209 \isamarkupfalse% |
205 \isamarkupfalse% |
210 \isacommand{end}\isanewline |
206 \isacommand{end}\isanewline |
211 \isanewline |
207 \isanewline |