equal
deleted
inserted
replaced
95 \isamarkuptrue% |
95 \isamarkuptrue% |
96 % |
96 % |
97 \medskip\begin{minipage}{0.6\textwidth} |
97 \medskip\begin{minipage}{0.6\textwidth} |
98 % |
98 % |
99 \isadelimproof |
99 \isadelimproof |
100 % |
100 \ \ \ \ % |
101 \endisadelimproof |
101 \endisadelimproof |
102 % |
102 % |
103 \isatagproof |
103 \isatagproof |
104 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
104 \isacommand{assume}\isamarkupfalse% |
105 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline |
105 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline |
106 \ \ \ \ \isacommand{then}\isamarkupfalse% |
106 \ \ \ \ \isacommand{then}\isamarkupfalse% |
107 \ \isacommand{have}\isamarkupfalse% |
107 \ \isacommand{have}\isamarkupfalse% |
108 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
108 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
109 % |
109 % |
133 final proof step via the \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} command:% |
133 final proof step via the \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} command:% |
134 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
135 \isamarkuptrue% |
135 \isamarkuptrue% |
136 % |
136 % |
137 \isadelimproof |
137 \isadelimproof |
138 % |
138 \ \ \ \ % |
139 \endisadelimproof |
139 \endisadelimproof |
140 % |
140 % |
141 \isatagproof |
141 \isatagproof |
142 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
142 \isacommand{assume}\isamarkupfalse% |
143 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline |
143 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline |
144 \ \ \ \ \isacommand{then}\isamarkupfalse% |
144 \ \ \ \ \isacommand{then}\isamarkupfalse% |
145 \ \isacommand{have}\isamarkupfalse% |
145 \ \isacommand{have}\isamarkupfalse% |
146 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
146 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
147 \ {\isacharparenleft}rule\ IntI{\isacharparenright}% |
147 \ {\isacharparenleft}rule\ IntI{\isacharparenright}% |
164 \isamarkuptrue% |
164 \isamarkuptrue% |
165 % |
165 % |
166 \medskip\begin{minipage}{0.6\textwidth} |
166 \medskip\begin{minipage}{0.6\textwidth} |
167 % |
167 % |
168 \isadelimproof |
168 \isadelimproof |
169 % |
169 \ \ \ \ % |
170 \endisadelimproof |
170 \endisadelimproof |
171 % |
171 % |
172 \isatagproof |
172 \isatagproof |
173 \ \ \ \ \isacommand{have}\isamarkupfalse% |
173 \isacommand{have}\isamarkupfalse% |
174 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline |
174 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline |
175 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
175 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
176 \isanewline |
176 \isanewline |
177 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
177 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
178 \ A\isanewline |
178 \ A\isanewline |
196 % |
196 % |
197 \endisatagnoproof |
197 \endisatagnoproof |
198 {\isafoldnoproof}% |
198 {\isafoldnoproof}% |
199 % |
199 % |
200 \isadelimnoproof |
200 \isadelimnoproof |
201 \isanewline |
201 % |
202 % |
202 \endisadelimnoproof |
203 \endisadelimnoproof |
203 \isanewline |
204 % |
204 % |
205 \isadelimproof |
205 \isadelimproof |
206 \ \ \ \ % |
206 \ \ \ \ % |
207 \endisadelimproof |
207 \endisadelimproof |
208 % |
208 % |
249 \isamarkuptrue% |
249 \isamarkuptrue% |
250 % |
250 % |
251 \medskip\begin{minipage}{0.6\textwidth} |
251 \medskip\begin{minipage}{0.6\textwidth} |
252 % |
252 % |
253 \isadelimproof |
253 \isadelimproof |
254 % |
254 \ \ \ \ % |
255 \endisadelimproof |
255 \endisadelimproof |
256 % |
256 % |
257 \isatagproof |
257 \isatagproof |
258 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
258 \isacommand{assume}\isamarkupfalse% |
259 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline |
259 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline |
260 \ \ \ \ \isacommand{then}\isamarkupfalse% |
260 \ \ \ \ \isacommand{then}\isamarkupfalse% |
261 \ \isacommand{have}\isamarkupfalse% |
261 \ \isacommand{have}\isamarkupfalse% |
262 \ C\isanewline |
262 \ C\isanewline |
263 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
263 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
284 % |
284 % |
285 \endisatagnoproof |
285 \endisatagnoproof |
286 {\isafoldnoproof}% |
286 {\isafoldnoproof}% |
287 % |
287 % |
288 \isadelimnoproof |
288 \isadelimnoproof |
289 \isanewline |
289 % |
290 % |
290 \endisadelimnoproof |
291 \endisadelimnoproof |
291 \isanewline |
292 % |
292 % |
293 \isadelimproof |
293 \isadelimproof |
294 \ \ \ \ % |
294 \ \ \ \ % |
295 \endisadelimproof |
295 \endisadelimproof |
296 % |
296 % |
324 elimination proof more conveniently:% |
324 elimination proof more conveniently:% |
325 \end{isamarkuptext}% |
325 \end{isamarkuptext}% |
326 \isamarkuptrue% |
326 \isamarkuptrue% |
327 % |
327 % |
328 \isadelimproof |
328 \isadelimproof |
329 % |
329 \ \ \ \ % |
330 \endisadelimproof |
330 \endisadelimproof |
331 % |
331 % |
332 \isatagproof |
332 \isatagproof |
333 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
333 \isacommand{assume}\isamarkupfalse% |
334 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline |
334 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline |
335 \ \ \ \ \isacommand{then}\isamarkupfalse% |
335 \ \ \ \ \isacommand{then}\isamarkupfalse% |
336 \ \isacommand{obtain}\isamarkupfalse% |
336 \ \isacommand{obtain}\isamarkupfalse% |
337 \ A\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
337 \ A\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
338 % |
338 % |
1184 \ B% |
1184 \ B% |
1185 \endisatagproof |
1185 \endisatagproof |
1186 {\isafoldproof}% |
1186 {\isafoldproof}% |
1187 % |
1187 % |
1188 \isadelimproof |
1188 \isadelimproof |
1189 \isanewline |
1189 % |
1190 % |
1190 \endisadelimproof |
1191 \endisadelimproof |
1191 \isanewline |
1192 % |
1192 % |
1193 \isadelimnoproof |
1193 \isadelimnoproof |
1194 \ \ \ \ \ \ % |
1194 \ \ \ \ \ \ % |
1195 \endisadelimnoproof |
1195 \endisadelimnoproof |
1196 % |
1196 % |
1199 % |
1199 % |
1200 \endisatagnoproof |
1200 \endisatagnoproof |
1201 {\isafoldnoproof}% |
1201 {\isafoldnoproof}% |
1202 % |
1202 % |
1203 \isadelimnoproof |
1203 \isadelimnoproof |
1204 \isanewline |
1204 % |
1205 % |
1205 \endisadelimnoproof |
1206 \endisadelimnoproof |
1206 \isanewline |
1207 % |
1207 % |
1208 \isadelimproof |
1208 \isadelimproof |
1209 \ \ % |
1209 \ \ % |
1210 \endisadelimproof |
1210 \endisadelimproof |
1211 % |
1211 % |
1266 \isamarkuptrue% |
1266 \isamarkuptrue% |
1267 % |
1267 % |
1268 \begin{minipage}{0.5\textwidth} |
1268 \begin{minipage}{0.5\textwidth} |
1269 % |
1269 % |
1270 \isadelimproof |
1270 \isadelimproof |
1271 % |
1271 \ \ % |
1272 \endisadelimproof |
1272 \endisadelimproof |
1273 % |
1273 % |
1274 \isatagproof |
1274 \isatagproof |
1275 \ \ \isacommand{have}\isamarkupfalse% |
1275 \isacommand{have}\isamarkupfalse% |
1276 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1276 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline |
1277 \ \ \isacommand{proof}\isamarkupfalse% |
1277 \ \ \isacommand{proof}\isamarkupfalse% |
1278 \ {\isacharminus}\isanewline |
1278 \ {\isacharminus}\isanewline |
1279 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
1279 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
1280 \ x\ \isakeyword{and}\ y\isanewline |
1280 \ x\ \isakeyword{and}\ y\isanewline |
1298 % |
1298 % |
1299 \endisatagnoproof |
1299 \endisatagnoproof |
1300 {\isafoldnoproof}% |
1300 {\isafoldnoproof}% |
1301 % |
1301 % |
1302 \isadelimnoproof |
1302 \isadelimnoproof |
1303 \isanewline |
1303 % |
1304 % |
1304 \endisadelimnoproof |
1305 \endisadelimnoproof |
1305 \isanewline |
1306 % |
1306 % |
1307 \isadelimproof |
1307 \isadelimproof |
1308 \ \ % |
1308 \ \ % |
1309 \endisadelimproof |
1309 \endisadelimproof |
1310 % |
1310 % |
1340 % |
1340 % |
1341 \endisatagnoproof |
1341 \endisatagnoproof |
1342 {\isafoldnoproof}% |
1342 {\isafoldnoproof}% |
1343 % |
1343 % |
1344 \isadelimnoproof |
1344 \isadelimnoproof |
1345 \isanewline |
1345 % |
1346 % |
1346 \endisadelimnoproof |
1347 \endisadelimnoproof |
1347 \isanewline |
1348 % |
1348 % |
1349 \isadelimproof |
1349 \isadelimproof |
1350 \ \ % |
1350 \ \ % |
1351 \endisadelimproof |
1351 \endisadelimproof |
1352 % |
1352 % |
1454 establish the intermediate results:% |
1454 establish the intermediate results:% |
1455 \end{isamarkuptext}% |
1455 \end{isamarkuptext}% |
1456 \isamarkuptrue% |
1456 \isamarkuptrue% |
1457 % |
1457 % |
1458 \isadelimproof |
1458 \isadelimproof |
1459 % |
1459 \ \ % |
1460 \endisadelimproof |
1460 \endisadelimproof |
1461 % |
1461 % |
1462 \isatagproof |
1462 \isatagproof |
1463 \ \ \isacommand{have}\isamarkupfalse% |
1463 \isacommand{have}\isamarkupfalse% |
1464 \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1464 \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1465 \isanewline |
1465 \isanewline |
1466 \ \ \isacommand{also}\isamarkupfalse% |
1466 \ \ \isacommand{also}\isamarkupfalse% |
1467 \ \isacommand{have}\isamarkupfalse% |
1467 \ \isacommand{have}\isamarkupfalse% |
1468 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ c{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |
1468 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ c{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% |