-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
47 lines (47 loc) · 158 KB
/
index.html
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
46
47
<!DOCTYPE html><html><head><meta charset="utf-8"><meta http-equiv="x-ua-compatible" content="ie=edge"><meta property="fb:app_id" content="118554188236439"><meta name="viewport" content="width=device-width, initial-scale=1"><meta name="author" content="Maxim Sokhatsky"><meta name="twitter:site" content="@5HT"><meta name="twitter:creator" content="@5HT"><meta property="og:type" content="website"><meta property="og:image" content="https://avatars.githubusercontent.com/u/17128096?s=400&u=66a63d4cdd9625b2b4b37d724cc00fe6401e5bd8&v=4"><meta name="msapplication-TileColor" content="#ffffff"><meta name="msapplication-TileImage" content="https://anders.groupoid.space/images/ms-icon-144x144.png"><meta name="theme-color" content="#ffffff"><link rel="stylesheet" href="https://anders.groupoid.space/main.css?v=1"><link rel="apple-touch-icon" sizes="57x57" href="https://anders.groupoid.space/images/apple-icon-57x57.png"><link rel="apple-touch-icon" sizes="60x60" href="https://anders.groupoid.space/images/apple-icon-60x60.png"><link rel="apple-touch-icon" sizes="72x72" href="https://anders.groupoid.space/images/apple-icon-72x72.png"><link rel="apple-touch-icon" sizes="76x76" href="https://anders.groupoid.space/images/apple-icon-76x76.png"><link rel="apple-touch-icon" sizes="114x114" href="https://anders.groupoid.space/images/apple-icon-114x114.png"><link rel="apple-touch-icon" sizes="120x120" href="https://anders.groupoid.space/images/apple-icon-120x120.png"><link rel="apple-touch-icon" sizes="144x144" href="https://anders.groupoid.space/images/apple-icon-144x144.png"><link rel="apple-touch-icon" sizes="152x152" href="https://anders.groupoid.space/images/apple-icon-152x152.png"><link rel="apple-touch-icon" sizes="180x180" href="https://anders.groupoid.space/images//apple-icon-180x180.png"><link rel="icon" type="image/png" sizes="192x192" href="https://anders.groupoid.space/images/android-icon-192x192.png"><link rel="icon" type="image/png" sizes="32x32" href="https://anders.groupoid.space/images/favicon-32x32.png"><link rel="icon" type="image/png" sizes="96x96" href="https://anders.groupoid.space/images/favicon-96x96.png"><link rel="icon" type="image/png" sizes="16x16" href="https://anders.groupoid.space/images/favicon-16x16.png"><link rel="manifest" href="https://anders.groupoid.space/images/manifest.json"><style>svg a{fill:blue;stroke:blue}
[data-mml-node="merror"]>g{fill:red;stroke:red}
[data-mml-node="merror"]>rect[data-background]{fill:yellow;stroke:none}
[data-frame],[data-line]{stroke-width:70px;fill:none}
.mjx-dashed{stroke-dasharray:140}
.mjx-dotted{stroke-linecap:round;stroke-dasharray:0,140}
use[data-c]{stroke-width:3px}
</style></head><body class="content"></body></html><html><head><meta property="og:title" content="LAURENT"><meta property="og:description" content="Analytical Type Theory"><meta property="og:url" content="https://laurent.groupoid.space/"></head></html><title>LAURENT</title><nav><a href='#'>LAURENT</a>
<a href='https://laurent.groupoid.space/mathematics/tutorial/'>TUTORIAL</a></nav><article class="main"><div class="exe"><section><h1>ANALYTICAL TYPE SYSTEM</h1></section><aside><time>Published: 28 FEB 2025 LOSAR</time><p>MLTT-72 based Type Theory for mechanical formalization
of Théorie des Distributions and Analyse Mathematique
by Laurent Schwartz and Foundation of Constructive Analysis by Errett Bishop.
</p><p>We omit identity types Id, idp, J (HoTT, MLTT-80, MLTT-75) to keep
the system lean with Pi and Set truncated Sigma relying instead on
Prop predicates. Also we have explicitly built in set theory with
open sets and topology to have more classical core.
Built-in inequalities propositional resolution by reduction
is handled by external Z3 SMT solver.
</p></aside><section><div class="macro"><div class="macro__col"><h3 id="hts"><b>MLTT</b></h3><ol><li><a href="https://laurent.groupoid.space/foundations/prop/">PROP</a></li><li><a href="https://laurent.groupoid.space/foundations/universe/">U<sub>0</sub> : U<sub>1</sub></a></li><li><a href="https://laurent.groupoid.space/foundations/forall/">FORALL</a></li><li><a href="https://laurent.groupoid.space/foundations/exists/">EXISTS</a></li><li><a href="https://laurent.groupoid.space/foundations/and/">AND</a></li><li><a href="https://laurent.groupoid.space/foundations/or/">OR</a></li><li><a href="https://laurent.groupoid.space/foundations/real/">REAL</a></li></ol></div><div class="macro__col"><h3 id="mltt"><b>SET</b></h3><ol><li><a href="https://laurent.groupoid.space/foundations/set/">SET</a></li><li><a href="https://laurent.groupoid.space/foundations/seteq/">EQ<sub><b>Z3</b></sub></a></li><li><a href="https://laurent.groupoid.space/foundations/complement/">\</a></li><li><a href="https://laurent.groupoid.space/foundations/intersect/">INTERSECT</a></li><li><a href="https://laurent.groupoid.space/foundations/closure/">CLOSURE</a></li><li><a href="https://laurent.groupoid.space/foundations/power/">POWER</a></li><li><a href="https://laurent.groupoid.space/foundations/quotient/">QUOTIENT</a></li></ol></div><div class="macro__col"><h3 id="mltt"><b>CALC</b></h3><ol><li><a href="https://laurent.groupoid.space/foundations/seq/">SEQ</a></li><li><a href="https://laurent.groupoid.space/foundations/inf/">INF</a></li><li><a href="https://laurent.groupoid.space/foundations/sup/">SUP</a></li><li><a href="https://laurent.groupoid.space/foundations/limit/">LIMIT</a></li><li><a href="https://laurent.groupoid.space/foundations/sum/">SUM</a></li><li><a href="https://laurent.groupoid.space/foundations/union/">UNION</a></li><li><a href="https://laurent.groupoid.space/foundations/measure/">MEASURE</a></li><li><a href="https://laurent.groupoid.space/foundations/lebesgue/">LEBESGUE</a></li><li><a href="https://laurent.groupoid.space/foundations/bochner/">BOCHER</a></li></ol></div></div><br><br><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="12.923ex" height="1.586ex" role="img" focusable="false" viewBox="0 -695 5712 701" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1014-TEX-B-1D408" d="M397 0Q370 3 218 3Q65 3 38 0H25V62H139V624H25V686H38Q65 683 218 683Q370 683 397 686H410V624H296V62H410V0H397Z"></path><path id="MJX-1014-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1014-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path><path id="MJX-1014-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-1014-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-1014-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-1014-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-1014-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D408" xlink:href="#MJX-1014-TEX-B-1D408"></use><use data-c="1D427" xlink:href="#MJX-1014-TEX-B-1D427" transform="translate(436,0)"></use><use data-c="1D42C" xlink:href="#MJX-1014-TEX-B-1D42C" transform="translate(1075,0)"></use><use data-c="1D42D" xlink:href="#MJX-1014-TEX-B-1D42D" transform="translate(1529,0)"></use><use data-c="1D41A" xlink:href="#MJX-1014-TEX-B-1D41A" transform="translate(1976,0)"></use><use data-c="1D425" xlink:href="#MJX-1014-TEX-B-1D425" transform="translate(2535,0)"></use><use data-c="1D425" xlink:href="#MJX-1014-TEX-B-1D425" transform="translate(2854,0)"></use><use data-c="1D41A" xlink:href="#MJX-1014-TEX-B-1D41A" transform="translate(3173,0)"></use><use data-c="1D42D" xlink:href="#MJX-1014-TEX-B-1D42D" transform="translate(3732,0)"></use><use data-c="1D422" xlink:href="#MJX-1014-TEX-B-1D422" transform="translate(4179,0)"></use><use data-c="1D428" xlink:href="#MJX-1014-TEX-B-1D428" transform="translate(4498,0)"></use><use data-c="1D427" xlink:href="#MJX-1014-TEX-B-1D427" transform="translate(5073,0)"></use></g></g></g></g></svg></mjx-container>.</p><p>The <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="7.833ex" height="1.57ex" role="img" focusable="false" viewBox="0 -683 3462 694" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1015-TEX-N-4C" d="M128 622Q121 629 117 631T101 634T58 637H25V683H36Q48 680 182 680Q324 680 348 683H360V637H333Q273 637 258 635T233 622L232 342V129Q232 57 237 52Q243 47 313 47Q384 47 410 53Q470 70 498 110T536 221Q536 226 537 238T540 261T542 272T562 273H582V268Q580 265 568 137T554 5V0H25V46H58Q100 47 109 49T128 61V622Z"></path><path id="MJX-1015-TEX-N-61" d="M137 305T115 305T78 320T63 359Q63 394 97 421T218 448Q291 448 336 416T396 340Q401 326 401 309T402 194V124Q402 76 407 58T428 40Q443 40 448 56T453 109V145H493V106Q492 66 490 59Q481 29 455 12T400 -6T353 12T329 54V58L327 55Q325 52 322 49T314 40T302 29T287 17T269 6T247 -2T221 -8T190 -11Q130 -11 82 20T34 107Q34 128 41 147T68 188T116 225T194 253T304 268H318V290Q318 324 312 340Q290 411 215 411Q197 411 181 410T156 406T148 403Q170 388 170 359Q170 334 154 320ZM126 106Q126 75 150 51T209 26Q247 26 276 49T315 109Q317 116 318 175Q318 233 317 233Q309 233 296 232T251 223T193 203T147 166T126 106Z"></path><path id="MJX-1015-TEX-N-75" d="M383 58Q327 -10 256 -10H249Q124 -10 105 89Q104 96 103 226Q102 335 102 348T96 369Q86 385 36 385H25V408Q25 431 27 431L38 432Q48 433 67 434T105 436Q122 437 142 438T172 441T184 442H187V261Q188 77 190 64Q193 49 204 40Q224 26 264 26Q290 26 311 35T343 58T363 90T375 120T379 144Q379 145 379 161T380 201T380 248V315Q380 361 370 372T320 385H302V431Q304 431 378 436T457 442H464V264Q464 84 465 81Q468 61 479 55T524 46H542V0Q540 0 467 -5T390 -11H383V58Z"></path><path id="MJX-1015-TEX-N-72" d="M36 46H50Q89 46 97 60V68Q97 77 97 91T98 122T98 161T98 203Q98 234 98 269T98 328L97 351Q94 370 83 376T38 385H20V408Q20 431 22 431L32 432Q42 433 60 434T96 436Q112 437 131 438T160 441T171 442H174V373Q213 441 271 441H277Q322 441 343 419T364 373Q364 352 351 337T313 322Q288 322 276 338T263 372Q263 381 265 388T270 400T273 405Q271 407 250 401Q234 393 226 386Q179 341 179 207V154Q179 141 179 127T179 101T180 81T180 66V61Q181 59 183 57T188 54T193 51T200 49T207 48T216 47T225 47T235 46T245 46H276V0H267Q249 3 140 3Q37 3 28 0H20V46H36Z"></path><path id="MJX-1015-TEX-N-65" d="M28 218Q28 273 48 318T98 391T163 433T229 448Q282 448 320 430T378 380T406 316T415 245Q415 238 408 231H126V216Q126 68 226 36Q246 30 270 30Q312 30 342 62Q359 79 369 104L379 128Q382 131 395 131H398Q415 131 415 121Q415 117 412 108Q393 53 349 21T250 -11Q155 -11 92 58T28 218ZM333 275Q322 403 238 411H236Q228 411 220 410T195 402T166 381T143 340T127 274V267H333V275Z"></path><path id="MJX-1015-TEX-N-6E" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 122T103 161T103 203Q103 234 103 269T102 328V351Q99 370 88 376T43 385H25V408Q25 431 27 431L37 432Q47 433 65 434T102 436Q119 437 138 438T167 441T178 442H181V402Q181 364 182 364T187 369T199 384T218 402T247 421T285 437Q305 442 336 442Q450 438 463 329Q464 322 464 190V104Q464 66 466 59T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1015-TEX-N-74" d="M27 422Q80 426 109 478T141 600V615H181V431H316V385H181V241Q182 116 182 100T189 68Q203 29 238 29Q282 29 292 100Q293 108 293 146V181H333V146V134Q333 57 291 17Q264 -10 221 -10Q187 -10 162 2T124 33T105 68T98 100Q97 107 97 248V385H18V422H27Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mtext"><use data-c="4C" xlink:href="#MJX-1015-TEX-N-4C"></use><use data-c="61" xlink:href="#MJX-1015-TEX-N-61" transform="translate(625,0)"></use><use data-c="75" xlink:href="#MJX-1015-TEX-N-75" transform="translate(1125,0)"></use><use data-c="72" xlink:href="#MJX-1015-TEX-N-72" transform="translate(1681,0)"></use><use data-c="65" xlink:href="#MJX-1015-TEX-N-65" transform="translate(2073,0)"></use><use data-c="6E" xlink:href="#MJX-1015-TEX-N-6E" transform="translate(2517,0)"></use><use data-c="74" xlink:href="#MJX-1015-TEX-N-74" transform="translate(3073,0)"></use></g></g></g></svg></mjx-container> doesn't have proper syntax yet,
that's said you use it as OCaml framework
working in pure AST as you would do in Lisp.
</p><code>$ git clone \
[email protected]<span class="h__symbol">:</span>groupoid/laurent
$ opam install z3
$ ocamlfind ocamlc -o laurent \
-package z3 -linkpkg src/laurent.ml
</code></section><section><h1>SYNTAX</h1><p style="text-align:center;"><mjx-container class="MathJax" jax="SVG" display="true"><svg style="vertical-align: -27.53ex;" xmlns="http://www.w3.org/2000/svg" width="43.827ex" height="56.191ex" role="img" focusable="false" viewBox="0 -12668.2 19371.6 24836.5" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1016-TEX-N-4C" d="M128 622Q121 629 117 631T101 634T58 637H25V683H36Q48 680 182 680Q324 680 348 683H360V637H333Q273 637 258 635T233 622L232 342V129Q232 57 237 52Q243 47 313 47Q384 47 410 53Q470 70 498 110T536 221Q536 226 537 238T540 261T542 272T562 273H582V268Q580 265 568 137T554 5V0H25V46H58Q100 47 109 49T128 61V622Z"></path><path id="MJX-1016-TEX-N-61" d="M137 305T115 305T78 320T63 359Q63 394 97 421T218 448Q291 448 336 416T396 340Q401 326 401 309T402 194V124Q402 76 407 58T428 40Q443 40 448 56T453 109V145H493V106Q492 66 490 59Q481 29 455 12T400 -6T353 12T329 54V58L327 55Q325 52 322 49T314 40T302 29T287 17T269 6T247 -2T221 -8T190 -11Q130 -11 82 20T34 107Q34 128 41 147T68 188T116 225T194 253T304 268H318V290Q318 324 312 340Q290 411 215 411Q197 411 181 410T156 406T148 403Q170 388 170 359Q170 334 154 320ZM126 106Q126 75 150 51T209 26Q247 26 276 49T315 109Q317 116 318 175Q318 233 317 233Q309 233 296 232T251 223T193 203T147 166T126 106Z"></path><path id="MJX-1016-TEX-N-75" d="M383 58Q327 -10 256 -10H249Q124 -10 105 89Q104 96 103 226Q102 335 102 348T96 369Q86 385 36 385H25V408Q25 431 27 431L38 432Q48 433 67 434T105 436Q122 437 142 438T172 441T184 442H187V261Q188 77 190 64Q193 49 204 40Q224 26 264 26Q290 26 311 35T343 58T363 90T375 120T379 144Q379 145 379 161T380 201T380 248V315Q380 361 370 372T320 385H302V431Q304 431 378 436T457 442H464V264Q464 84 465 81Q468 61 479 55T524 46H542V0Q540 0 467 -5T390 -11H383V58Z"></path><path id="MJX-1016-TEX-N-72" d="M36 46H50Q89 46 97 60V68Q97 77 97 91T98 122T98 161T98 203Q98 234 98 269T98 328L97 351Q94 370 83 376T38 385H20V408Q20 431 22 431L32 432Q42 433 60 434T96 436Q112 437 131 438T160 441T171 442H174V373Q213 441 271 441H277Q322 441 343 419T364 373Q364 352 351 337T313 322Q288 322 276 338T263 372Q263 381 265 388T270 400T273 405Q271 407 250 401Q234 393 226 386Q179 341 179 207V154Q179 141 179 127T179 101T180 81T180 66V61Q181 59 183 57T188 54T193 51T200 49T207 48T216 47T225 47T235 46T245 46H276V0H267Q249 3 140 3Q37 3 28 0H20V46H36Z"></path><path id="MJX-1016-TEX-N-65" d="M28 218Q28 273 48 318T98 391T163 433T229 448Q282 448 320 430T378 380T406 316T415 245Q415 238 408 231H126V216Q126 68 226 36Q246 30 270 30Q312 30 342 62Q359 79 369 104L379 128Q382 131 395 131H398Q415 131 415 121Q415 117 412 108Q393 53 349 21T250 -11Q155 -11 92 58T28 218ZM333 275Q322 403 238 411H236Q228 411 220 410T195 402T166 381T143 340T127 274V267H333V275Z"></path><path id="MJX-1016-TEX-N-6E" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 122T103 161T103 203Q103 234 103 269T102 328V351Q99 370 88 376T43 385H25V408Q25 431 27 431L37 432Q47 433 65 434T102 436Q119 437 138 438T167 441T178 442H181V402Q181 364 182 364T187 369T199 384T218 402T247 421T285 437Q305 442 336 442Q450 438 463 329Q464 322 464 190V104Q464 66 466 59T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1016-TEX-N-74" d="M27 422Q80 426 109 478T141 600V615H181V431H316V385H181V241Q182 116 182 100T189 68Q203 29 238 29Q282 29 292 100Q293 108 293 146V181H333V146V134Q333 57 291 17Q264 -10 221 -10Q187 -10 162 2T124 33T105 68T98 100Q97 107 97 248V385H18V422H27Z"></path><path id="MJX-1016-TEX-N-3A" d="M78 370Q78 394 95 412T138 430Q162 430 180 414T199 371Q199 346 182 328T139 310T96 327T78 370ZM78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path id="MJX-1016-TEX-N-3D" d="M56 347Q56 360 70 367H707Q722 359 722 347Q722 336 708 328L390 327H72Q56 332 56 347ZM56 153Q56 168 72 173H708Q722 163 722 153Q722 140 707 133H70Q56 140 56 153Z"></path><path id="MJX-1016-TEX-N-4D" d="M132 622Q125 629 121 631T105 634T62 637H29V683H135Q221 683 232 682T249 675Q250 674 354 398L458 124L562 398Q666 674 668 675Q671 681 683 682T781 683H887V637H854Q814 636 803 634T785 622V61Q791 51 802 49T854 46H887V0H876Q855 3 736 3Q605 3 596 0H585V46H618Q660 47 669 49T688 61V347Q688 424 688 461T688 546T688 613L687 632Q454 14 450 7Q446 1 430 1T410 7Q409 9 292 316L176 624V606Q175 588 175 543T175 463T175 356L176 86Q187 50 261 46H278V0H269Q254 3 154 3Q52 3 37 0H29V46H46Q78 48 98 56T122 69T132 86V622Z"></path><path id="MJX-1016-TEX-N-54" d="M36 443Q37 448 46 558T55 671V677H666V671Q667 666 676 556T685 443V437H645V443Q645 445 642 478T631 544T610 593Q593 614 555 625Q534 630 478 630H451H443Q417 630 414 618Q413 616 413 339V63Q420 53 439 50T528 46H558V0H545L361 3Q186 1 177 0H164V46H194Q264 46 283 49T309 63V339V550Q309 620 304 625T271 630H244H224Q154 630 119 601Q101 585 93 554T81 486T76 443V437H36V443Z"></path><path id="MJX-1016-TEX-N-A0" d=""></path><path id="MJX-1016-TEX-N-7C" d="M139 -249H137Q125 -249 119 -235V251L120 737Q130 750 139 750Q152 750 159 735V-235Q151 -249 141 -249H139Z"></path><path id="MJX-1016-TEX-N-42" d="M131 622Q124 629 120 631T104 634T61 637H28V683H229H267H346Q423 683 459 678T531 651Q574 627 599 590T624 512Q624 461 583 419T476 360L466 357Q539 348 595 302T651 187Q651 119 600 67T469 3Q456 1 242 0H28V46H61Q103 47 112 49T131 61V622ZM511 513Q511 560 485 594T416 636Q415 636 403 636T371 636T333 637Q266 637 251 636T232 628Q229 624 229 499V374H312L396 375L406 377Q410 378 417 380T442 393T474 417T499 456T511 513ZM537 188Q537 239 509 282T430 336L329 337H229V200V116Q229 57 234 52Q240 47 334 47H383Q425 47 443 53Q486 67 511 104T537 188Z"></path><path id="MJX-1016-TEX-N-73" d="M295 316Q295 356 268 385T190 414Q154 414 128 401Q98 382 98 349Q97 344 98 336T114 312T157 287Q175 282 201 278T245 269T277 256Q294 248 310 236T342 195T359 133Q359 71 321 31T198 -10H190Q138 -10 94 26L86 19L77 10Q71 4 65 -1L54 -11H46H42Q39 -11 33 -5V74V132Q33 153 35 157T45 162H54Q66 162 70 158T75 146T82 119T101 77Q136 26 198 26Q295 26 295 104Q295 133 277 151Q257 175 194 187T111 210Q75 227 54 256T33 318Q33 357 50 384T93 424T143 442T187 447H198Q238 447 268 432L283 424L292 431Q302 440 314 448H322H326Q329 448 335 442V310L329 304H301Q295 310 295 316Z"></path><path id="MJX-1016-TEX-N-53" d="M55 507Q55 590 112 647T243 704H257Q342 704 405 641L426 672Q431 679 436 687T446 700L449 704Q450 704 453 704T459 705H463Q466 705 472 699V462L466 456H448Q437 456 435 459T430 479Q413 605 329 646Q292 662 254 662Q201 662 168 626T135 542Q135 508 152 480T200 435Q210 431 286 412T370 389Q427 367 463 314T500 191Q500 110 448 45T301 -21Q245 -21 201 -4T140 27L122 41Q118 36 107 21T87 -7T78 -21Q76 -22 68 -22H64Q61 -22 55 -16V101Q55 220 56 222Q58 227 76 227H89Q95 221 95 214Q95 182 105 151T139 90T205 42T305 24Q352 24 386 62T420 155Q420 198 398 233T340 281Q284 295 266 300Q261 301 239 306T206 314T174 325T141 343T112 367T85 402Q55 451 55 507Z"></path><path id="MJX-1016-TEX-N-51" d="M56 341Q56 499 157 602T388 705Q521 705 621 601T722 341Q722 275 703 218T660 127T603 63T555 25T525 9Q524 8 524 8H523Q524 5 526 -1T537 -21T555 -47T581 -67T615 -76Q653 -76 678 -56T706 -3Q707 10 716 10Q721 10 728 5L727 -13Q727 -88 697 -140T606 -193Q563 -193 538 -166T498 -83Q483 -23 483 -8L471 -11Q459 -14 435 -18T388 -22Q254 -22 155 81T56 341ZM607 339Q607 429 586 496T531 598T461 649T390 665T318 649T248 598T192 496T170 339Q170 143 277 57Q301 39 305 39L304 42Q304 44 304 46Q301 53 301 68Q301 101 325 128T391 155Q454 155 495 70L501 58Q549 91 578 164Q607 234 607 339ZM385 18Q404 18 425 23T459 33T472 40Q471 47 468 57T449 88T412 115Q398 117 386 117Q367 117 353 102T338 67Q338 48 351 33T385 18Z"></path><path id="MJX-1016-TEX-N-69" d="M69 609Q69 637 87 653T131 669Q154 667 171 652T188 609Q188 579 171 564T129 549Q104 549 87 564T69 609ZM247 0Q232 3 143 3Q132 3 106 3T56 1L34 0H26V46H42Q70 46 91 49Q100 53 102 60T104 102V205V293Q104 345 102 359T88 378Q74 385 41 385H30V408Q30 431 32 431L42 432Q52 433 70 434T106 436Q123 437 142 438T171 441T182 442H185V62Q190 52 197 50T232 46H255V0H247Z"></path><path id="MJX-1016-TEX-N-6D" d="M41 46H55Q94 46 102 60V68Q102 77 102 91T102 122T103 161T103 203Q103 234 103 269T102 328V351Q99 370 88 376T43 385H25V408Q25 431 27 431L37 432Q47 433 65 434T102 436Q119 437 138 438T167 441T178 442H181V402Q181 364 182 364T187 369T199 384T218 402T247 421T285 437Q305 442 336 442Q351 442 364 440T387 434T406 426T421 417T432 406T441 395T448 384T452 374T455 366L457 361L460 365Q463 369 466 373T475 384T488 397T503 410T523 422T546 432T572 439T603 442Q729 442 740 329Q741 322 741 190V104Q741 66 743 59T754 49Q775 46 803 46H819V0H811L788 1Q764 2 737 2T699 3Q596 3 587 0H579V46H595Q656 46 656 62Q657 64 657 200Q656 335 655 343Q649 371 635 385T611 402T585 404Q540 404 506 370Q479 343 472 315T464 232V168V108Q464 78 465 68T468 55T477 49Q498 46 526 46H542V0H534L510 1Q487 2 460 2T422 3Q319 3 310 0H302V46H318Q379 46 379 62Q380 64 380 200Q379 335 378 343Q372 371 358 385T334 402T308 404Q263 404 229 370Q202 343 195 315T187 232V168V108Q187 78 188 68T191 55T200 49Q221 46 249 46H265V0H257L234 1Q210 2 183 2T145 3Q42 3 33 0H25V46H41Z"></path><path id="MJX-1016-TEX-N-63" d="M370 305T349 305T313 320T297 358Q297 381 312 396Q317 401 317 402T307 404Q281 408 258 408Q209 408 178 376Q131 329 131 219Q131 137 162 90Q203 29 272 29Q313 29 338 55T374 117Q376 125 379 127T395 129H409Q415 123 415 120Q415 116 411 104T395 71T366 33T318 2T249 -11Q163 -11 99 53T34 214Q34 318 99 383T250 448T370 421T404 357Q404 334 387 320Z"></path><path id="MJX-1016-TEX-N-6F" d="M28 214Q28 309 93 378T250 448Q340 448 405 380T471 215Q471 120 407 55T250 -10Q153 -10 91 57T28 214ZM250 30Q372 30 372 193V225V250Q372 272 371 288T364 326T348 362T317 390T268 410Q263 411 252 411Q222 411 195 399Q152 377 139 338T126 246V226Q126 130 145 91Q177 30 250 30Z"></path><path id="MJX-1016-TEX-N-76" d="M338 431Q344 429 422 429Q479 429 503 431H508V385H497Q439 381 423 345Q421 341 356 172T288 -2Q283 -11 263 -11Q244 -11 239 -2Q99 359 98 364Q93 378 82 381T43 385H19V431H25L33 430Q41 430 53 430T79 430T104 429T122 428Q217 428 232 431H240V385H226Q187 384 184 370Q184 366 235 234L286 102L377 341V349Q377 363 367 372T349 383T335 385H331V431H338Z"></path><path id="MJX-1016-TEX-N-66" d="M273 0Q255 3 146 3Q43 3 34 0H26V46H42Q70 46 91 49Q99 52 103 60Q104 62 104 224V385H33V431H104V497L105 564L107 574Q126 639 171 668T266 704Q267 704 275 704T289 705Q330 702 351 679T372 627Q372 604 358 590T321 576T284 590T270 627Q270 647 288 667H284Q280 668 273 668Q245 668 223 647T189 592Q183 572 182 497V431H293V385H185V225Q185 63 186 61T189 57T194 54T199 51T206 49T213 48T222 47T231 47T241 46T251 46H282V0H273Z"></path><path id="MJX-1016-TEX-N-6C" d="M42 46H56Q95 46 103 60V68Q103 77 103 91T103 124T104 167T104 217T104 272T104 329Q104 366 104 407T104 482T104 542T103 586T103 603Q100 622 89 628T44 637H26V660Q26 683 28 683L38 684Q48 685 67 686T104 688Q121 689 141 690T171 693T182 694H185V379Q185 62 186 60Q190 52 198 49Q219 46 247 46H263V0H255L232 1Q209 2 183 2T145 3T107 3T57 1L34 0H26V46H42Z"></path><path id="MJX-1016-TEX-N-78" d="M201 0Q189 3 102 3Q26 3 17 0H11V46H25Q48 47 67 52T96 61T121 78T139 96T160 122T180 150L226 210L168 288Q159 301 149 315T133 336T122 351T113 363T107 370T100 376T94 379T88 381T80 383Q74 383 44 385H16V431H23Q59 429 126 429Q219 429 229 431H237V385Q201 381 201 369Q201 367 211 353T239 315T268 274L272 270L297 304Q329 345 329 358Q329 364 327 369T322 376T317 380T310 384L307 385H302V431H309Q324 428 408 428Q487 428 493 431H499V385H492Q443 385 411 368Q394 360 377 341T312 257L296 236L358 151Q424 61 429 57T446 50Q464 46 499 46H516V0H510H502Q494 1 482 1T457 2T432 2T414 3Q403 3 377 3T327 1L304 0H295V46H298Q309 46 320 51T331 63Q331 65 291 120L250 175Q249 174 219 133T185 88Q181 83 181 74Q181 63 188 55T206 46Q208 46 208 23V0H201Z"></path><path id="MJX-1016-TEX-B-1D40F" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H253Q435 686 470 685T536 678Q585 668 621 648T675 605T705 557T718 514T721 483T718 451T704 409T673 362T616 322T530 293Q500 288 399 287H304V62H412V0H400ZM553 475Q553 554 537 582T459 622Q451 623 373 624H298V343H372Q457 344 480 350Q527 362 540 390T553 475Z"></path><path id="MJX-1016-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-1016-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-1016-TEX-B-1D429" d="M32 442L123 446Q214 450 215 450H221V409Q222 409 229 413T251 423T284 436T328 446T382 450Q480 450 540 388T600 223Q600 128 539 61T361 -6H354Q292 -6 236 28L227 34V-132H296V-194H287Q269 -191 163 -191Q56 -191 38 -194H29V-132H98V113V284Q98 330 97 348T93 370T83 376Q69 380 42 380H29V442H32ZM457 224Q457 303 427 349T350 395Q282 395 235 352L227 345V104L233 97Q274 45 337 45Q383 45 420 86T457 224Z"></path><path id="MJX-1016-TEX-B-1D414" d="M570 686Q588 683 703 683T836 686H845V624H737V420Q737 390 737 345T738 284Q738 205 729 164T689 83Q614 -11 465 -11Q321 -11 240 51T148 207Q147 214 147 421V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V405V370V268Q304 181 311 146T346 87Q387 52 466 52Q642 52 667 195Q668 204 669 415V624H561V686H570Z"></path><path id="MJX-1016-TEX-B-1D7CE" d="M266 654H280H282Q500 654 524 418Q529 370 529 320Q529 125 456 52Q397 -10 287 -10Q110 -10 63 154Q45 212 45 316Q45 504 113 585Q140 618 185 636T266 654ZM374 548Q347 604 286 604Q247 604 218 575Q197 552 193 511T188 311Q188 159 196 116Q202 87 225 64T287 41Q339 41 367 87Q379 107 382 152T386 329Q386 518 374 548Z"></path><path id="MJX-1016-TEX-B-1D7CF" d="M481 0L294 3Q136 3 109 0H96V62H227V304Q227 546 225 546Q169 529 97 529H80V591H97Q231 591 308 647L319 655H333Q355 655 359 644Q361 640 361 351V62H494V0H481Z"></path><path id="MJX-1016-TEX-B-1D42F" d="M401 444Q413 441 495 441Q568 441 574 444H580V382H510L409 156Q348 18 339 6Q331 -4 320 -4Q318 -4 313 -4T303 -3H288Q273 -3 264 12T221 102Q206 135 197 156L96 382H26V444H34Q49 441 145 441Q252 441 270 444H279V382H231L284 264Q335 149 338 149Q338 150 389 264T442 381Q442 382 418 382H394V444H401Z"></path><path id="MJX-1016-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-1016-TEX-N-64" d="M376 495Q376 511 376 535T377 568Q377 613 367 624T316 637H298V660Q298 683 300 683L310 684Q320 685 339 686T376 688Q393 689 413 690T443 693T454 694H457V390Q457 84 458 81Q461 61 472 55T517 46H535V0Q533 0 459 -5T380 -11H373V44L365 37Q307 -11 235 -11Q158 -11 96 50T34 215Q34 315 97 378T244 442Q319 442 376 393V495ZM373 342Q328 405 260 405Q211 405 173 369Q146 341 139 305T131 211Q131 155 138 120T173 59Q203 26 251 26Q322 26 373 103V342Z"></path><path id="MJX-1016-TEX-B-1D421" d="M40 686L131 690Q222 694 223 694H229V533L230 372L238 381Q248 394 264 407T317 435T398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V332Q106 387 106 453T107 534Q107 593 105 605T91 620Q77 624 50 624H37V686H40Z"></path><path id="MJX-1016-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-1016-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-1016-TEX-N-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path><path id="MJX-1016-TEX-N-45" d="M128 619Q121 626 117 628T101 631T58 634H25V680H597V676Q599 670 611 560T625 444V440H585V444Q584 447 582 465Q578 500 570 526T553 571T528 601T498 619T457 629T411 633T353 634Q266 634 251 633T233 622Q233 622 233 621Q232 619 232 497V376H286Q359 378 377 385Q413 401 416 469Q416 471 416 473V493H456V213H416V233Q415 268 408 288T383 317T349 328T297 330Q290 330 286 330H232V196V114Q232 57 237 52Q243 47 289 47H340H391Q428 47 452 50T505 62T552 92T584 146Q594 172 599 200T607 247T612 270V273H652V270Q651 267 632 137T610 3V0H25V46H58Q100 47 109 49T128 61V619Z"></path><path id="MJX-1016-TEX-I-1D706" d="M166 673Q166 685 183 694H202Q292 691 316 644Q322 629 373 486T474 207T524 67Q531 47 537 34T546 15T551 6T555 2T556 -2T550 -11H482Q457 3 450 18T399 152L354 277L340 262Q327 246 293 207T236 141Q211 112 174 69Q123 9 111 -1T83 -12Q47 -12 47 20Q47 37 61 52T199 187Q229 216 266 252T321 306L338 322Q338 323 288 462T234 612Q214 657 183 657Q166 657 166 673Z"></path><path id="MJX-1016-TEX-N-2203" d="M56 661T56 674T70 694H487Q497 686 500 679V15Q497 10 487 1L279 0H70Q56 7 56 20T70 40H460V327H84Q70 334 70 347T84 367H460V654H70Q56 661 56 674Z"></path><path id="MJX-1016-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-1016-TEX-N-2C" d="M78 35T78 60T94 103T137 121Q165 121 187 96T210 8Q210 -27 201 -60T180 -117T154 -158T130 -185T117 -194Q113 -194 104 -185T95 -172Q95 -168 106 -156T131 -126T157 -76T173 -3V9L172 8Q170 7 167 6T161 3T152 1T140 0Q113 0 96 17Z"></path><path id="MJX-1016-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path id="MJX-1016-TEX-B-2E" d="M74 85Q74 121 99 146T156 171Q200 171 222 143T245 85Q245 56 224 29T160 1Q118 1 96 27T74 85Z"></path><path id="MJX-1016-TEX-B-1D7D0" d="M175 580Q175 578 185 572T205 551T215 510Q215 467 191 449T137 430Q107 430 83 448T58 511Q58 558 91 592T168 640T259 654Q328 654 383 637Q451 610 484 563T517 459Q517 401 482 360T368 262Q340 243 265 184L210 140H274Q416 140 429 145Q439 148 447 186T455 237H517V233Q516 230 501 119Q489 9 486 4V0H57V25Q57 51 58 54Q60 57 109 106T215 214T288 291Q364 377 364 458Q364 515 328 553T231 592Q214 592 201 589T181 584T175 580Z"></path><path id="MJX-1016-TEX-B-2115" d="M20 664Q20 666 31 683H142Q256 683 258 681Q259 680 279 653T342 572T422 468L582 259V425Q582 451 582 490T583 541Q583 611 573 628T522 648Q500 648 493 654Q484 665 493 679L500 683H691Q702 676 702 666Q702 657 698 652Q688 648 680 648Q633 648 627 612Q624 601 624 294V-8Q616 -20 607 -20Q601 -20 596 -15Q593 -13 371 270L156 548L153 319Q153 284 153 234T152 167Q152 103 156 78T172 44T213 34Q236 34 242 28Q253 17 242 3L236 -1H36Q24 6 24 16Q24 34 56 34Q58 35 69 36T86 40T100 50T109 72Q111 83 111 345V603L96 619Q72 643 44 648Q20 648 20 664ZM413 419L240 648H120L136 628Q137 626 361 341T587 54L589 68Q589 78 589 121V192L413 419Z"></path><path id="MJX-1016-TEX-N-2124" d="M39 -1Q29 9 29 12Q29 23 60 77T219 337L410 648H364Q261 648 210 628Q168 612 142 588T109 545T97 509T88 490Q85 489 80 489Q72 489 61 503L70 588Q72 607 75 628T79 662T81 675Q84 677 88 681Q90 683 341 683H592Q604 673 604 666Q604 662 412 348L221 37Q221 35 301 35Q406 35 446 48Q504 68 543 111T597 212Q602 239 617 239Q624 239 629 234T635 223Q635 215 621 113T604 8L597 1Q595 -1 317 -1H39ZM148 637L166 648H112V632Q111 629 110 622T108 612Q108 608 110 608T116 612T129 623T148 637ZM552 646Q552 648 504 648Q452 648 450 643Q448 639 266 343T77 37Q77 35 128 35H179L366 339L552 646ZM572 35Q581 89 581 97L561 77Q542 59 526 48L508 37L539 35H572Z"></path><path id="MJX-1016-TEX-N-211A" d="M480 -10Q480 -13 486 -24T507 -50T541 -80T588 -104T648 -114Q666 -114 688 -110T714 -106Q724 -106 728 -114T729 -130Q723 -145 663 -163T548 -181Q503 -181 463 -169T395 -139T343 -97T307 -56T284 -19L280 -3L262 1Q188 24 131 81Q57 155 37 275Q34 292 34 342T37 410Q58 528 131 601Q179 652 248 676T388 701Q485 701 562 661Q698 595 731 448Q742 410 742 341T731 235Q707 141 646 81Q616 50 575 27T493 -5L480 -10ZM568 342Q568 613 437 659L395 666Q329 666 286 626Q232 570 213 439Q210 408 210 342T213 246Q231 113 286 57Q309 37 342 23Q357 19 389 19Q420 19 437 23Q469 38 491 57Q568 134 568 342ZM174 341V354Q174 393 175 419T183 484T205 561T246 635L249 639Q246 639 224 627T193 608Q189 606 183 601T169 589T155 577Q69 491 69 344Q69 133 231 52Q247 42 247 46Q247 46 246 48Q231 69 222 85T200 141T177 239Q174 269 174 341ZM708 341Q708 410 689 467T640 556T588 606T546 630Q532 638 531 638Q530 638 531 635Q563 590 577 543Q602 472 602 341V316Q602 264 599 230T580 144T531 48Q529 44 532 45T546 52Q575 68 596 84T642 128T683 200T706 299Q708 327 708 341ZM391 -17H333Q329 -15 326 -15Q324 -15 324 -17Q324 -21 362 -68Q424 -130 506 -143Q518 -144 544 -144Q569 -144 577 -143L589 -141L575 -139Q544 -127 509 -101T453 -37L442 -19L391 -17Z"></path><path id="MJX-1016-TEX-N-211D" d="M17 665Q17 672 28 683H221Q415 681 439 677Q461 673 481 667T516 654T544 639T566 623T584 607T597 592T607 578T614 565T618 554L621 548Q626 530 626 497Q626 447 613 419Q578 348 473 326L455 321Q462 310 473 292T517 226T578 141T637 72T686 35Q705 30 705 16Q705 7 693 -1H510Q503 6 404 159L306 310H268V183Q270 67 271 59Q274 42 291 38Q295 37 319 35Q344 35 353 28Q362 17 353 3L346 -1H28Q16 5 16 16Q16 35 55 35Q96 38 101 52Q106 60 106 341T101 632Q95 645 55 648Q17 648 17 665ZM241 35Q238 42 237 45T235 78T233 163T233 337V621L237 635L244 648H133Q136 641 137 638T139 603T141 517T141 341Q141 131 140 89T134 37Q133 36 133 35H241ZM457 496Q457 540 449 570T425 615T400 634T377 643Q374 643 339 648Q300 648 281 635Q271 628 270 610T268 481V346H284Q327 346 375 352Q421 364 439 392T457 496ZM492 537T492 496T488 427T478 389T469 371T464 361Q464 360 465 360Q469 360 497 370Q593 400 593 495Q593 592 477 630L457 637L461 626Q474 611 488 561Q492 537 492 496ZM464 243Q411 317 410 317Q404 317 401 315Q384 315 370 312H346L526 35H619L606 50Q553 109 464 243Z"></path><path id="MJX-1016-TEX-N-2102" d="M684 131Q684 125 672 109T633 71T573 29T489 -5T386 -19Q330 -19 276 -3T174 46T91 134T44 261Q39 283 39 341T44 421Q66 538 143 611T341 699Q344 699 364 700T395 701Q449 698 503 677T585 655Q603 655 611 662T620 678T625 694T639 702Q650 702 657 690V481L653 474Q640 467 628 472Q624 476 618 496T595 541Q562 587 507 625T390 663H381Q337 663 299 625Q212 547 212 336Q212 249 233 179Q274 30 405 30Q533 30 641 130Q658 147 666 147Q671 147 677 143T684 131ZM250 625Q264 643 261 643Q238 635 214 620T161 579T110 510T79 414Q74 384 74 341T79 268Q89 213 113 169T164 101T217 61T260 39L277 34Q270 41 264 48Q199 111 181 254Q178 281 178 344T181 434Q200 559 250 625ZM621 565V625Q617 623 613 623Q603 619 590 619H575L588 605Q608 583 610 579L621 565Z"></path><path id="MJX-1016-TEX-N-210D" d="M14 666Q14 675 26 683H344L351 679Q361 665 351 655Q344 648 317 648Q287 645 282 641Q270 637 269 623T266 497V370H511V497Q511 519 510 553Q509 615 507 626T496 641H495Q489 645 459 648Q420 648 420 665Q420 672 426 679L433 683H751Q762 676 762 666Q762 648 724 648Q684 645 677 632Q675 626 675 341Q675 57 677 52Q684 38 724 35Q762 35 762 16Q762 6 751 -1H433L426 3Q420 10 420 17Q420 35 459 35Q501 38 506 52Q511 64 511 190V323H266V190Q266 60 271 52Q276 38 317 35Q342 35 351 28Q360 17 351 3L344 -1H26Q14 5 14 16Q14 35 53 35Q94 38 99 52Q104 60 104 341T99 632Q93 645 53 648Q14 648 14 666ZM233 341V553Q233 635 239 648H131Q134 641 135 638T137 603T139 517T139 341Q139 131 138 89T132 37Q131 36 131 35H239Q233 47 233 129V341ZM639 341V489Q639 548 639 576T640 620T642 639T646 648H537L542 639Q546 625 546 341Q546 130 545 88T538 37Q537 36 537 35H646Q643 41 643 42T641 55T639 84T639 140V341Z"></path><path id="MJX-1016-TEX-N-1D546" d="M131 601Q180 652 249 676T387 701Q485 701 562 661Q628 629 671 575T731 448Q742 410 742 341T731 234Q707 140 646 81Q549 -19 389 -19Q228 -19 131 81Q57 155 37 274Q34 292 34 341Q34 392 37 410Q58 528 131 601ZM568 341Q568 613 437 659Q406 664 395 665Q329 665 286 625Q232 571 213 439Q210 408 210 341Q210 275 213 245Q232 111 286 57Q309 37 342 23Q357 19 389 19Q420 19 437 23Q469 38 491 57Q568 132 568 341ZM174 341Q174 403 177 441T197 535T249 639Q246 639 224 627T193 608Q189 606 183 601T169 589T155 577Q69 488 69 344Q69 133 231 52Q244 45 246 45Q248 45 246 48Q231 69 222 85T200 141T177 239Q174 269 174 341ZM708 341Q708 415 684 475T635 563T582 610Q578 612 565 619T546 630Q533 637 531 637Q530 637 530 636V635L531 634Q562 591 577 543Q602 471 602 341V316Q602 264 599 230T580 144T531 48L530 47V46Q530 45 531 45Q533 45 547 52T583 75T622 105Q708 195 708 341Z"></path><path id="MJX-1016-TEX-N-1D54D" d="M316 683Q327 676 327 666Q327 648 302 648Q272 642 258 628Q249 621 249 608Q252 589 263 556T289 485T322 406T357 325T388 256T411 205L420 185Q423 185 473 317Q547 497 547 590Q547 621 541 632T516 648Q501 648 498 654Q488 664 498 679L504 683H607H660Q695 683 707 680T719 667Q719 660 714 654T700 648Q678 648 658 628L642 614L513 301Q484 231 449 148T397 25T380 -15Q373 -20 368 -20Q361 -20 358 -15Q354 -13 287 135T149 438T67 610Q45 648 18 648Q11 648 6 653T0 666Q0 677 9 680T59 683H164H316ZM216 614Q216 620 216 622T216 628T216 633T217 635T218 638T219 640T221 644T224 648H84L96 632Q118 592 236 330L367 43L387 88L404 132L380 185Q250 468 222 568Q216 590 216 614ZM576 645Q584 628 584 597L587 568L598 597Q609 624 618 637L624 648H600Q576 648 576 645Z"></path><path id="MJX-1016-TEX-B-1D412" d="M64 493Q64 582 120 636T264 696H272Q280 697 285 697Q380 697 454 645L480 669Q484 672 488 676T495 683T500 688T504 691T508 693T511 695T514 696T517 697T522 697Q536 697 539 691T542 652V577Q542 557 542 532T543 500Q543 472 540 465T524 458H511H505Q489 458 485 461T479 478Q472 529 449 564T393 614T336 634T287 639Q228 639 203 610T177 544Q177 517 195 493T247 457Q253 454 343 436T475 391Q574 326 574 207V200Q574 163 559 120Q517 12 389 -9Q380 -10 346 -10Q308 -10 275 -5T221 7T184 22T160 35T151 40L126 17Q122 14 118 10T111 3T106 -2T102 -5T98 -7T95 -9T92 -10T89 -11T84 -11Q70 -11 67 -4T64 35V108Q64 128 64 153T63 185Q63 203 63 211T69 223T77 227T94 228H100Q118 228 122 225T126 205Q130 125 193 88T345 51Q408 51 434 82T460 157Q460 196 439 221T388 257Q384 259 305 276T221 295Q155 313 110 366T64 493Z"></path><path id="MJX-1016-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-1016-TEX-B-1D42A" d="M38 220Q38 273 54 314T95 380T152 421T211 443T264 449Q368 449 429 386L438 377L484 450H540V-132H609V-194H600Q582 -191 475 -191Q360 -191 351 -194H342V-132H411V42Q409 41 399 34T383 25T367 16T347 7T324 1T296 -4T264 -6Q162 -6 100 56T38 220ZM287 46Q368 46 417 127V301L412 312Q398 347 369 371T302 395Q282 395 263 388T225 362T194 308T182 221Q182 126 214 86T287 46Z"></path><path id="MJX-1016-TEX-B-1D404" d="M723 286Q721 284 700 145T677 3V0H39V62H147V618H39V680H660V676Q662 670 675 552T691 428V424H629V428Q629 429 627 448T618 494T601 541Q574 593 527 605T382 618H374H304V384H336Q338 384 347 384T361 384T376 386T392 390T407 397T421 407T432 423Q442 444 443 482V501H505V205H443V224Q442 258 435 278T411 307T380 318T336 322H304V62H375H394Q429 62 449 62T497 66T541 76T577 95T609 126T632 170T651 232Q661 287 661 289H723V286Z"></path><path id="MJX-1016-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-1016-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1016-TEX-B-1D41D" d="M351 686L442 690Q533 694 534 694H540V389Q540 327 540 253T539 163Q539 97 541 83T555 66Q569 62 596 62H609V31Q609 0 608 0Q588 0 510 -3T412 -6Q411 -6 411 16V38L401 31Q337 -6 265 -6Q159 -6 99 58T38 224Q38 265 51 303T92 375T165 429T272 449Q359 449 417 412V507V555Q417 597 415 607T402 620Q388 624 361 624H348V686H351ZM411 350Q362 399 291 399Q278 399 256 392T218 371Q195 351 189 320T182 238V221Q182 179 183 159T191 115T212 74Q241 46 288 46Q358 46 404 100L411 109V350Z"></path><path id="MJX-1016-TEX-B-1D40E" d="M64 339Q64 431 96 502T182 614T295 675T420 696Q469 696 481 695Q620 680 709 589T798 339Q798 173 697 82T432 -10Q262 -10 163 85T64 339ZM625 454Q618 502 600 538T562 593T515 624T469 639T431 642Q331 642 276 563Q232 493 232 353Q232 315 234 285T244 216T267 148T308 94T372 56Q405 46 432 46Q517 46 567 106T627 267Q631 299 631 353Q631 418 625 454Z"></path><path id="MJX-1016-TEX-B-1D402" d="M64 343Q64 502 174 599T468 697Q502 697 533 691T586 674T623 655T647 639T657 632L694 663Q703 670 711 677T723 687T730 692T735 695T740 696T746 697Q759 697 762 692T766 668V627V489V449Q766 428 762 424T742 419H732H720Q699 419 697 436Q690 498 657 545Q611 618 532 632Q522 634 496 634Q356 634 286 553Q232 488 232 343T286 133Q355 52 497 52Q597 52 650 112T704 237Q704 248 709 251T729 254H735Q750 254 755 253T763 248T766 234Q766 136 680 63T469 -11Q285 -11 175 86T64 343Z"></path><path id="MJX-1016-TEX-B-1D426" d="M40 442Q217 450 218 450H224V365Q226 367 235 378T254 397T278 416T314 435T362 448Q376 450 400 450H406Q503 450 534 393Q545 376 545 370Q545 368 555 379Q611 450 716 450Q774 450 809 434Q850 414 861 379T873 276V213V198V62H942V0H933Q915 3 809 3Q702 3 684 0H675V62H744V194V275Q744 348 735 373T690 399Q645 399 607 370T557 290Q555 281 554 171V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1016-TEX-B-1D408" d="M397 0Q370 3 218 3Q65 3 38 0H25V62H139V624H25V686H38Q65 683 218 683Q370 683 397 686H410V624H296V62H410V0H397Z"></path><path id="MJX-1016-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path><path id="MJX-1016-TEX-B-1D41C" d="M447 131H458Q478 131 478 117Q478 112 471 95T439 51T377 9Q330 -6 286 -6Q196 -6 135 35Q39 96 39 222Q39 324 101 384Q169 453 286 453Q359 453 411 431T464 353Q464 319 445 302T395 284Q360 284 343 305T325 353Q325 380 338 396H333Q317 398 295 398H292Q280 398 271 397T245 390T218 373T197 338T183 283Q182 275 182 231Q182 199 184 180T193 132T220 85T270 57Q289 50 317 50H326Q385 50 414 115Q419 127 423 129T447 131Z"></path><path id="MJX-1016-TEX-B-1D430" d="M624 444Q636 441 722 441Q797 441 800 444H805V382H741L593 11Q592 10 590 8T586 4T584 2T581 0T579 -2T575 -3T571 -3T567 -4T561 -4T553 -4H542Q525 -4 518 6T490 70Q474 110 463 137L415 257L367 137Q357 111 341 72Q320 17 313 7T289 -4H277Q259 -4 253 -2T238 11L90 382H25V444H32Q47 441 140 441Q243 441 261 444H270V382H222L310 164L382 342L366 382H303V444H310Q322 441 407 441Q508 441 523 444H531V382H506Q481 382 481 380Q482 376 529 259T577 142L674 382H617V444H624Z"></path><path id="MJX-1016-TEX-B-1D42E" d="M40 442L134 446Q228 450 229 450H235V273V165Q235 90 238 74T254 52Q268 46 304 46H319Q352 46 380 67T419 121L420 123Q424 135 425 199Q425 201 425 207Q425 233 425 249V316Q425 354 423 363T410 376Q396 380 369 380H356V442L554 450V267Q554 84 556 79Q561 62 610 62H623V31Q623 0 622 0Q603 0 527 -3T432 -6Q431 -6 431 25V56L420 45Q373 6 332 -1Q313 -6 281 -6Q208 -6 165 14T109 87L107 98L106 230Q106 358 104 366Q96 380 50 380H37V442H40Z"></path><path id="MJX-1016-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-1016-TEX-B-2212" d="M119 221Q96 230 96 251T116 279Q121 281 448 281H775Q776 280 779 278T785 274T791 269T795 262T797 251Q797 230 775 221H119Z"></path><path id="MJX-1016-TEX-B-2F" d="M451 730Q460 750 479 750Q492 750 501 740T510 718Q508 708 318 244L122 -232Q112 -250 95 -250Q82 -250 73 -241T64 -218Q66 -205 258 261T451 730Z"></path><path id="MJX-1016-TEX-N-223C" d="M55 166Q55 241 101 304T222 367Q260 367 296 349T362 304T421 252T484 208T554 189Q616 189 655 236T694 338Q694 350 698 358T708 367Q722 367 722 334Q722 260 677 197T562 134H554Q517 134 481 152T414 196T355 248T292 293T223 311Q179 311 145 286Q109 257 96 218T80 156T69 133Q55 133 55 166Z"></path><path id="MJX-1016-TEX-B-1D410" d="M64 339Q64 431 96 502T182 614T295 675T420 696Q469 696 481 695Q620 680 709 589T798 339Q798 255 768 184Q720 77 611 26L600 21Q635 -26 682 -26H696Q769 -26 769 0Q769 7 774 12T787 18Q805 18 805 -7V-13Q803 -64 785 -106T737 -171Q720 -183 697 -191Q687 -193 668 -193Q636 -193 613 -182T575 -144T552 -94T532 -27Q531 -23 530 -16T528 -6T526 -3L512 -5Q499 -7 477 -8T431 -10Q393 -10 382 -9Q238 8 151 97T64 339ZM326 80Q326 113 356 138T430 163Q492 163 542 100L553 86Q554 85 561 91T578 108Q637 179 637 330Q637 430 619 498T548 604Q500 641 425 641Q408 641 390 637T347 623T299 590T259 535Q226 469 226 338Q226 244 246 180T318 79L325 74Q326 74 326 80ZM506 58Q480 112 433 112Q412 112 395 104T378 77Q378 44 431 44Q480 44 506 58Z"></path><path id="MJX-1016-TEX-B-1D40B" d="M643 285Q641 280 629 148T612 4V0H39V62H147V624H39V686H51Q75 683 228 683Q415 685 425 686H439V624H304V62H352H378Q492 62 539 138Q551 156 558 178T569 214T576 255T581 289H643V285Z"></path><path id="MJX-1016-TEX-B-1D41F" d="M308 0Q290 3 172 3Q58 3 49 0H40V62H109V382H42V444H109V503L110 562L112 572Q127 625 178 658T316 699Q318 699 330 699T348 700Q381 698 404 687T436 658T449 629T452 606Q452 576 432 557T383 537Q355 537 335 555T314 605Q314 635 328 649H325Q311 649 293 644T253 618T227 560Q226 555 226 498V444H340V382H232V62H318V0H308Z"></path><path id="MJX-1016-TEX-B-1D40C" d="M314 0Q296 3 181 3T48 0H39V62H147V624H39V686H305Q316 679 323 667Q330 653 434 414L546 157L658 414Q766 662 773 674Q778 681 788 686H1052V624H944V62H1052V0H1040Q1016 3 874 3T708 0H696V62H804V341L803 618L786 580Q770 543 735 462T671 315Q540 13 536 9Q528 1 507 1Q485 1 477 9Q472 14 408 162T281 457T217 603Q215 603 215 334V62H323V0H314Z"></path><path id="MJX-1016-TEX-B-1D41B" d="M32 686L123 690Q214 694 215 694H221V409Q289 450 378 450Q479 450 539 387T600 221Q600 122 535 58T358 -6H355Q272 -6 203 53L160 1L129 0H98V301Q98 362 98 435T99 525Q99 591 97 604T83 620Q69 624 42 624H29V686H32ZM227 105L232 99Q237 93 242 87T258 73T280 59T306 49T339 45Q380 45 411 66T451 131Q457 160 457 230Q457 264 456 284T448 329T430 367T396 389T343 398Q282 398 235 355L227 348V105Z"></path><path id="MJX-1016-TEX-B-1D420" d="M50 300Q50 368 105 409T255 450Q328 450 376 426L388 420Q435 455 489 455Q517 455 533 441T554 414T558 389Q558 367 544 353T508 339Q484 339 471 354T458 387Q458 397 462 400Q464 401 461 400Q459 400 454 399Q429 392 427 390Q454 353 459 328Q461 315 461 300Q461 240 419 202Q364 149 248 149Q185 149 136 172Q129 158 129 148Q129 105 170 93Q176 91 263 91Q273 91 298 91T334 91T366 89T400 85T432 77T466 64Q544 22 544 -69Q544 -114 506 -145Q438 -201 287 -201Q149 -201 90 -161T30 -70Q30 -58 33 -47T42 -27T54 -13T69 -1T82 6T94 12T101 15Q66 57 66 106Q66 151 90 187L97 197L89 204Q50 243 50 300ZM485 403H492Q491 404 488 404L485 403V403ZM255 200Q279 200 295 206T319 219T331 242T335 268T336 300Q336 337 333 352T317 380Q298 399 255 399Q228 399 211 392T187 371T178 345T176 312V300V289Q176 235 194 219Q215 200 255 200ZM287 -150Q357 -150 400 -128T443 -71Q443 -65 442 -61T436 -50T420 -37T389 -27T339 -21L308 -20Q276 -20 253 -20Q190 -20 180 -20T156 -26Q130 -38 130 -69Q130 -105 173 -127T287 -150Z"></path><path id="MJX-1016-TEX-B-1D401" d="M720 510Q720 476 704 448T665 404T619 377T580 362L564 359L583 356Q602 353 632 342T690 312Q712 292 725 276Q752 235 752 189V183Q752 160 741 125Q698 18 547 2Q543 1 288 0H39V62H147V624H39V686H264H409Q502 686 542 681T624 655Q720 607 720 510ZM563 513Q563 553 548 578T518 611T486 622Q479 624 385 624H293V382H375Q458 383 467 385Q563 405 563 513ZM590 192Q590 307 505 329Q504 330 503 330L398 331H293V62H391H400H444Q496 62 528 75T580 131Q590 155 590 192Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mtable"><g data-mml-node="mtr" transform="translate(0,11918.2)"><g data-mml-node="mtd" transform="translate(9685.8,0)"></g></g><g data-mml-node="mtr" transform="translate(0,10518.2)"><g data-mml-node="mtd"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="4C" xlink:href="#MJX-1016-TEX-N-4C"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(625,0)"></use><use data-c="75" xlink:href="#MJX-1016-TEX-N-75" transform="translate(1125,0)"></use><use data-c="72" xlink:href="#MJX-1016-TEX-N-72" transform="translate(1681,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(2073,0)"></use><use data-c="6E" xlink:href="#MJX-1016-TEX-N-6E" transform="translate(2517,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(3073,0)"></use></g></g><g data-mml-node="mo" transform="translate(3739.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5073.6,0)"><g data-mml-node="mi"><use data-c="4D" xlink:href="#MJX-1016-TEX-N-4D"></use><use data-c="4C" xlink:href="#MJX-1016-TEX-N-4C" transform="translate(917,0)"></use><use data-c="54" xlink:href="#MJX-1016-TEX-N-54" transform="translate(1542,0)"></use><use data-c="54" xlink:href="#MJX-1016-TEX-N-54" transform="translate(2264,0)"></use></g></g><g data-mml-node="mtext" transform="translate(8059.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8309.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(8587.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8837.6,0)"><g data-mml-node="mi"><use data-c="42" xlink:href="#MJX-1016-TEX-N-42"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(708,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(1208,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(1602,0)"></use></g></g><g data-mml-node="mtext" transform="translate(10883.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11133.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(11411.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11661.6,0)"><g data-mml-node="mi"><use data-c="53" xlink:href="#MJX-1016-TEX-N-53"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(556,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1000,0)"></use></g></g><g data-mml-node="mtext" transform="translate(13050.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13300.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(13578.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13828.6,0)"><g data-mml-node="mi"><use data-c="51" xlink:href="#MJX-1016-TEX-N-51"></use></g></g><g data-mml-node="mtext" transform="translate(14606.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(14856.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(15134.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(15384.6,0)"><g data-mml-node="mi"><use data-c="4D" xlink:href="#MJX-1016-TEX-N-4D"></use><use data-c="75" xlink:href="#MJX-1016-TEX-N-75" transform="translate(917,0)"></use></g></g><g data-mml-node="mtext" transform="translate(16857.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(17107.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(17385.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(17635.6,0)"><g data-mml-node="mi"><use data-c="4C" xlink:href="#MJX-1016-TEX-N-4C"></use><use data-c="69" xlink:href="#MJX-1016-TEX-N-69" transform="translate(625,0)"></use><use data-c="6D" xlink:href="#MJX-1016-TEX-N-6D" transform="translate(903,0)"></use></g></g></g></g><g data-mml-node="mtr" transform="translate(0,9118.2)"><g data-mml-node="mtd" transform="translate(1512,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="4D" xlink:href="#MJX-1016-TEX-N-4D"></use><use data-c="4C" xlink:href="#MJX-1016-TEX-N-4C" transform="translate(917,0)"></use><use data-c="54" xlink:href="#MJX-1016-TEX-N-54" transform="translate(1542,0)"></use><use data-c="54" xlink:href="#MJX-1016-TEX-N-54" transform="translate(2264,0)"></use></g></g><g data-mml-node="mo" transform="translate(3263.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4597.6,0)"><g data-mml-node="mi"><use data-c="63" xlink:href="#MJX-1016-TEX-N-63"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(444,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(944,0)"></use><use data-c="6D" xlink:href="#MJX-1016-TEX-N-6D" transform="translate(1338,0)"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(2171,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(2671,0)"></use></g></g><g data-mml-node="mtext" transform="translate(7662.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7912.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(8190.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8440.6,0)"><g data-mml-node="mi"><use data-c="76" xlink:href="#MJX-1016-TEX-N-76"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(528,0)"></use><use data-c="72" xlink:href="#MJX-1016-TEX-N-72" transform="translate(1028,0)"></use></g></g><g data-mml-node="mtext" transform="translate(9860.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(10110.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(10388.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(10638.6,0)"><g data-mml-node="mi"><use data-c="66" xlink:href="#MJX-1016-TEX-N-66"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(306,0)"></use><use data-c="72" xlink:href="#MJX-1016-TEX-N-72" transform="translate(806,0)"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(1198,0)"></use><use data-c="6C" xlink:href="#MJX-1016-TEX-N-6C" transform="translate(1698,0)"></use><use data-c="6C" xlink:href="#MJX-1016-TEX-N-6C" transform="translate(1976,0)"></use></g></g><g data-mml-node="mtext" transform="translate(12892.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13142.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(13420.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13670.6,0)"><g data-mml-node="mi"><use data-c="65" xlink:href="#MJX-1016-TEX-N-65"></use><use data-c="78" xlink:href="#MJX-1016-TEX-N-78" transform="translate(444,0)"></use><use data-c="69" xlink:href="#MJX-1016-TEX-N-69" transform="translate(972,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(1250,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1644,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(2033,0)"></use></g></g><g data-mml-node="mtext" transform="translate(16097.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,7718.2)"><g data-mml-node="mtd" transform="translate(9685.8,0)"></g></g><g data-mml-node="mtr" transform="translate(0,6318.2)"><g data-mml-node="mtd" transform="translate(3402.4,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="63" xlink:href="#MJX-1016-TEX-N-63"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(444,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(944,0)"></use><use data-c="6D" xlink:href="#MJX-1016-TEX-N-6D" transform="translate(1338,0)"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(2171,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(2671,0)"></use></g></g><g data-mml-node="mo" transform="translate(3342.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4676.6,0)"><g data-mml-node="mi"><use data-c="1D40F" xlink:href="#MJX-1016-TEX-B-1D40F"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(786,0)"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(1260,0)"></use><use data-c="1D429" xlink:href="#MJX-1016-TEX-B-1D429" transform="translate(1835,0)"></use></g></g><g data-mml-node="mtext" transform="translate(7150.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="mo" transform="translate(7678.3,0)"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="mtext" transform="translate(8234.1,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8484.1,0)"><g data-mml-node="msub"><g data-mml-node="mi"><use data-c="1D414" xlink:href="#MJX-1016-TEX-B-1D414"></use></g><g data-mml-node="mn" transform="translate(918,-150) scale(0.707)"><use data-c="1D7CE" xlink:href="#MJX-1016-TEX-B-1D7CE"></use></g></g></g><g data-mml-node="mtext" transform="translate(9858.7,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="mo" transform="translate(10386.5,0)"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="mtext" transform="translate(10942.3,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11192.3,0)"><g data-mml-node="msub"><g data-mml-node="mi"><use data-c="1D414" xlink:href="#MJX-1016-TEX-B-1D414"></use></g><g data-mml-node="mn" transform="translate(918,-150) scale(0.707)"><use data-c="1D7CF" xlink:href="#MJX-1016-TEX-B-1D7CF"></use></g></g></g></g></g><g data-mml-node="mtr" transform="translate(0,4918.2)"><g data-mml-node="mtd" transform="translate(4694.5,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="76" xlink:href="#MJX-1016-TEX-N-76"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(528,0)"></use><use data-c="72" xlink:href="#MJX-1016-TEX-N-72" transform="translate(1028,0)"></use></g></g><g data-mml-node="mo" transform="translate(1697.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3031.6,0)"><g data-mml-node="mi"><use data-c="1D42F" xlink:href="#MJX-1016-TEX-B-1D42F"></use><use data-c="1D41A" xlink:href="#MJX-1016-TEX-B-1D41A" transform="translate(607,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(1166,0)"></use></g></g><g data-mml-node="mtext" transform="translate(4671.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4921.6,0)"><g data-mml-node="mi"><use data-c="69" xlink:href="#MJX-1016-TEX-N-69"></use><use data-c="64" xlink:href="#MJX-1016-TEX-N-64" transform="translate(278,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(834,0)"></use><use data-c="6E" xlink:href="#MJX-1016-TEX-N-6E" transform="translate(1278,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1834,0)"></use></g></g><g data-mml-node="mtext" transform="translate(7144.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7394.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(7672.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7922.6,0)"><g data-mml-node="mi"><use data-c="1D421" xlink:href="#MJX-1016-TEX-B-1D421"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(639,0)"></use><use data-c="1D425" xlink:href="#MJX-1016-TEX-B-1D425" transform="translate(1214,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(1533,0)"></use></g></g></g></g><g data-mml-node="mtr" transform="translate(0,3518.2)"><g data-mml-node="mtd" transform="translate(1264.5,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="66" xlink:href="#MJX-1016-TEX-N-66"></use><use data-c="6F" xlink:href="#MJX-1016-TEX-N-6F" transform="translate(306,0)"></use><use data-c="72" xlink:href="#MJX-1016-TEX-N-72" transform="translate(806,0)"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(1198,0)"></use><use data-c="6C" xlink:href="#MJX-1016-TEX-N-6C" transform="translate(1698,0)"></use><use data-c="6C" xlink:href="#MJX-1016-TEX-N-6C" transform="translate(1976,0)"></use></g></g><g data-mml-node="mo" transform="translate(2531.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="mi" transform="translate(3865.6,0)"><use data-c="2200" xlink:href="#MJX-1016-TEX-N-2200"></use></g><g data-mml-node="mtext" transform="translate(4421.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4671.6,0)"><g data-mml-node="mi"><use data-c="69" xlink:href="#MJX-1016-TEX-N-69"></use><use data-c="64" xlink:href="#MJX-1016-TEX-N-64" transform="translate(278,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(834,0)"></use><use data-c="6E" xlink:href="#MJX-1016-TEX-N-6E" transform="translate(1278,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1834,0)"></use></g></g><g data-mml-node="mtext" transform="translate(6894.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7144.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(7825.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8075.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(8756.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9006.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(9284.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="mi" transform="translate(9534.6,0)"><use data-c="1D706" xlink:href="#MJX-1016-TEX-I-1D706"></use></g><g data-mml-node="mtext" transform="translate(10117.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(10367.6,0)"><g data-mml-node="mi"><use data-c="69" xlink:href="#MJX-1016-TEX-N-69"></use><use data-c="64" xlink:href="#MJX-1016-TEX-N-64" transform="translate(278,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(834,0)"></use><use data-c="6E" xlink:href="#MJX-1016-TEX-N-6E" transform="translate(1278,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1834,0)"></use></g></g><g data-mml-node="mtext" transform="translate(12590.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12840.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(13521.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13771.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(14452.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(14702.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(14980.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(15230.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(15911.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(16161.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g></g></g><g data-mml-node="mtr" transform="translate(0,2118.2)"><g data-mml-node="mtd" transform="translate(1186.7,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="65" xlink:href="#MJX-1016-TEX-N-65"></use><use data-c="78" xlink:href="#MJX-1016-TEX-N-78" transform="translate(444,0)"></use><use data-c="69" xlink:href="#MJX-1016-TEX-N-69" transform="translate(972,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(1250,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1644,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(2033,0)"></use></g></g><g data-mml-node="mo" transform="translate(2704.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="mi" transform="translate(4038.6,0)"><use data-c="2203" xlink:href="#MJX-1016-TEX-N-2203"></use></g><g data-mml-node="mtext" transform="translate(4594.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4844.6,0)"><g data-mml-node="mi"><use data-c="69" xlink:href="#MJX-1016-TEX-N-69"></use><use data-c="64" xlink:href="#MJX-1016-TEX-N-64" transform="translate(278,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(834,0)"></use><use data-c="6E" xlink:href="#MJX-1016-TEX-N-6E" transform="translate(1278,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1834,0)"></use></g></g><g data-mml-node="mtext" transform="translate(7067.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7317.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(7998.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8248.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mtext" transform="translate(8929.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9179.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(9457.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="mo" transform="translate(9707.6,0)"><use data-c="28" xlink:href="#MJX-1016-TEX-N-28"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(10096.6,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mo" transform="translate(10777.6,0)"><use data-c="2C" xlink:href="#MJX-1016-TEX-N-2C"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11222.2,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="mo" transform="translate(11903.2,0)"><use data-c="29" xlink:href="#MJX-1016-TEX-N-29"></use></g><g data-mml-node="mtext" transform="translate(12292.2,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12542.2,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(12820.2,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13070.2,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13751.2,0)"><g data-mml-node="mn"><use data-c="2E" xlink:href="#MJX-1016-TEX-B-2E"></use><use data-c="1D7CF" xlink:href="#MJX-1016-TEX-B-1D7CF" transform="translate(319,0)"></use></g></g><g data-mml-node="mtext" transform="translate(14645.2,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(14895.2,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(15173.2,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(15423.2,0)"><g data-mml-node="mi"><use data-c="45" xlink:href="#MJX-1016-TEX-N-45"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(16104.2,0)"><g data-mml-node="mn"><use data-c="2E" xlink:href="#MJX-1016-TEX-B-2E"></use><use data-c="1D7D0" xlink:href="#MJX-1016-TEX-B-1D7D0" transform="translate(319,0)"></use></g></g></g></g><g data-mml-node="mtr" transform="translate(0,718.2)"><g data-mml-node="mtd" transform="translate(2064.5,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="42" xlink:href="#MJX-1016-TEX-N-42"></use><use data-c="61" xlink:href="#MJX-1016-TEX-N-61" transform="translate(708,0)"></use><use data-c="73" xlink:href="#MJX-1016-TEX-N-73" transform="translate(1208,0)"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(1602,0)"></use></g></g><g data-mml-node="mo" transform="translate(2323.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3657.6,0)"><g data-mml-node="mi"><use data-c="2115" xlink:href="#MJX-1016-TEX-B-2115"></use></g></g><g data-mml-node="mtext" transform="translate(4379.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4629.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(4907.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5157.6,0)"><g data-mml-node="mi"><use data-c="2124" xlink:href="#MJX-1016-TEX-N-2124"></use></g></g><g data-mml-node="mtext" transform="translate(5824.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(6074.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(6352.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(6602.6,0)"><g data-mml-node="mi"><use data-c="211A" xlink:href="#MJX-1016-TEX-N-211A"></use></g></g><g data-mml-node="mtext" transform="translate(7380.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7630.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(7908.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8158.6,0)"><g data-mml-node="mi"><use data-c="211D" xlink:href="#MJX-1016-TEX-N-211D"></use></g></g><g data-mml-node="mtext" transform="translate(8880.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9130.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(9408.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9658.6,0)"><g data-mml-node="mi"><use data-c="2102" xlink:href="#MJX-1016-TEX-N-2102"></use></g></g><g data-mml-node="mtext" transform="translate(10380.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(10630.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(10908.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11158.6,0)"><g data-mml-node="mi"><use data-c="210D" xlink:href="#MJX-1016-TEX-N-210D"></use></g></g><g data-mml-node="mtext" transform="translate(11936.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12186.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(12464.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12714.6,0)"><g data-mml-node="mi"><use data-c="1D546" xlink:href="#MJX-1016-TEX-N-1D546"></use></g></g><g data-mml-node="mtext" transform="translate(13492.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(13742.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(14020.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(14270.6,0)"><g data-mml-node="mi"><use data-c="1D54D" xlink:href="#MJX-1016-TEX-N-1D54D"></use></g></g><g data-mml-node="mtext" transform="translate(14992.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-681.8)"><g data-mml-node="mtd" transform="translate(2776.5,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="53" xlink:href="#MJX-1016-TEX-N-53"></use><use data-c="65" xlink:href="#MJX-1016-TEX-N-65" transform="translate(556,0)"></use><use data-c="74" xlink:href="#MJX-1016-TEX-N-74" transform="translate(1000,0)"></use></g></g><g data-mml-node="mo" transform="translate(1666.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3000.6,0)"><g data-mml-node="mi"><use data-c="1D412" xlink:href="#MJX-1016-TEX-B-1D412"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(639,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(1166,0)"></use></g></g><g data-mml-node="mtext" transform="translate(4613.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4863.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(5141.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5391.6,0)"><g data-mml-node="mi"><use data-c="1D412" xlink:href="#MJX-1016-TEX-B-1D412"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(639,0)"></use><use data-c="1D42A" xlink:href="#MJX-1016-TEX-B-1D42A" transform="translate(1166,0)"></use><use data-c="1D404" xlink:href="#MJX-1016-TEX-B-1D404" transform="translate(1773,0)"></use><use data-c="1D42A" xlink:href="#MJX-1016-TEX-B-1D42A" transform="translate(2529,0)"></use></g></g><g data-mml-node="mtext" transform="translate(8527.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8777.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(9055.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9305.6,0)"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-1016-TEX-B-1D400"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(869,0)"></use><use data-c="1D41D" xlink:href="#MJX-1016-TEX-B-1D41D" transform="translate(1508,0)"></use></g></g><g data-mml-node="mtext" transform="translate(11452.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11702.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(11980.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12230.6,0)"><g data-mml-node="mi"><use data-c="1D40E" xlink:href="#MJX-1016-TEX-B-1D40E"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(864,0)"></use></g></g><g data-mml-node="mtext" transform="translate(13568.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-2081.8)"><g data-mml-node="mtd" transform="translate(3466.8,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g><g data-mml-node="mtext" transform="translate(278,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(528,0)"><g data-mml-node="mi"><use data-c="1D402" xlink:href="#MJX-1016-TEX-B-1D402"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(831,0)"></use><use data-c="1D426" xlink:href="#MJX-1016-TEX-B-1D426" transform="translate(1406,0)"></use><use data-c="1D429" xlink:href="#MJX-1016-TEX-B-1D429" transform="translate(2364,0)"></use><use data-c="1D425" xlink:href="#MJX-1016-TEX-B-1D425" transform="translate(3003,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(3322,0)"></use><use data-c="1D426" xlink:href="#MJX-1016-TEX-B-1D426" transform="translate(3849,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(4807,0)"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(5334,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(5973,0)"></use></g></g><g data-mml-node="mtext" transform="translate(6948,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7198,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(7476,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7726,0)"><g data-mml-node="mi"><use data-c="1D408" xlink:href="#MJX-1016-TEX-B-1D408"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(436,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(1075,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(1522,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(2049,0)"></use><use data-c="1D42C" xlink:href="#MJX-1016-TEX-B-1D42C" transform="translate(2523,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(2977,0)"></use><use data-c="1D41C" xlink:href="#MJX-1016-TEX-B-1D41C" transform="translate(3504,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(4015,0)"></use></g></g><g data-mml-node="mtext" transform="translate(12188,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-3481.8)"><g data-mml-node="mtd" transform="translate(2843.3,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g><g data-mml-node="mtext" transform="translate(278,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(528,0)"><g data-mml-node="mi"><use data-c="1D40F" xlink:href="#MJX-1016-TEX-B-1D40F"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(786,0)"></use><use data-c="1D430" xlink:href="#MJX-1016-TEX-B-1D430" transform="translate(1361,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(2192,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(2719,0)"></use></g></g><g data-mml-node="mtext" transform="translate(3721,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3971,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(4249,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4499,0)"><g data-mml-node="mi"><use data-c="1D402" xlink:href="#MJX-1016-TEX-B-1D402"></use><use data-c="1D425" xlink:href="#MJX-1016-TEX-B-1D425" transform="translate(831,0)"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(1150,0)"></use><use data-c="1D42C" xlink:href="#MJX-1016-TEX-B-1D42C" transform="translate(1725,0)"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(2179,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(2818,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(3292,0)"></use></g></g><g data-mml-node="mtext" transform="translate(8318,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8568,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(8846,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(9096,0)"><g data-mml-node="mi"><use data-c="1D402" xlink:href="#MJX-1016-TEX-B-1D402"></use><use data-c="1D41A" xlink:href="#MJX-1016-TEX-B-1D41A" transform="translate(831,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(1390,0)"></use><use data-c="1D41D" xlink:href="#MJX-1016-TEX-B-1D41D" transform="translate(1864,0)"></use><use data-c="1D422" xlink:href="#MJX-1016-TEX-B-1D422" transform="translate(2503,0)"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(2822,0)"></use><use data-c="1D41A" xlink:href="#MJX-1016-TEX-B-1D41A" transform="translate(3461,0)"></use><use data-c="1D425" xlink:href="#MJX-1016-TEX-B-1D425" transform="translate(4020,0)"></use></g></g><g data-mml-node="mtext" transform="translate(13435,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-4881.8)"><g data-mml-node="mtd" transform="translate(2448.1,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="51" xlink:href="#MJX-1016-TEX-N-51"></use></g></g><g data-mml-node="mo" transform="translate(1055.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(2389.6,0)"><g data-mml-node="mo"><use data-c="2212" xlink:href="#MJX-1016-TEX-B-2212"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(894,0)"><g data-mml-node="mo"><use data-c="2F" xlink:href="#MJX-1016-TEX-B-2F"></use></g></g><g data-mml-node="mspace" transform="translate(1469,0)"></g><g data-mml-node="mo" transform="translate(1538,0)"><use data-c="223C" xlink:href="#MJX-1016-TEX-N-223C"></use></g></g><g data-mml-node="mtext" transform="translate(4705.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4955.5,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(5233.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5483.5,0)"><g data-mml-node="mi"><use data-c="1D410" xlink:href="#MJX-1016-TEX-B-1D410"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(864,0)"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(1503,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(2078,0)"></use></g></g><g data-mml-node="mtext" transform="translate(8008.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8258.5,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(8536.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8786.5,0)"><g data-mml-node="msub"><g data-mml-node="mi"><use data-c="1D40B" xlink:href="#MJX-1016-TEX-B-1D40B"></use><use data-c="1D422" xlink:href="#MJX-1016-TEX-B-1D422" transform="translate(692,0)"></use><use data-c="1D41F" xlink:href="#MJX-1016-TEX-B-1D41F" transform="translate(1011,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(1362,0)"></use></g><g data-mml-node="mi" transform="translate(1842,-150) scale(0.707)"><use data-c="1D410" xlink:href="#MJX-1016-TEX-B-1D410"></use></g></g></g><g data-mml-node="mtext" transform="translate(11289.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11539.5,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(11817.5,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(12067.5,0)"><g data-mml-node="msub"><g data-mml-node="mi"><use data-c="1D408" xlink:href="#MJX-1016-TEX-B-1D408"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(436,0)"></use><use data-c="1D41D" xlink:href="#MJX-1016-TEX-B-1D41D" transform="translate(1075,0)"></use></g><g data-mml-node="mi" transform="translate(1747,-150) scale(0.707)"><use data-c="1D410" xlink:href="#MJX-1016-TEX-B-1D410"></use></g></g></g></g></g><g data-mml-node="mtr" transform="translate(0,-6318.2)"><g data-mml-node="mtd" transform="translate(4628,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="4D" xlink:href="#MJX-1016-TEX-N-4D"></use><use data-c="75" xlink:href="#MJX-1016-TEX-N-75" transform="translate(917,0)"></use></g></g><g data-mml-node="mo" transform="translate(1750.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3084.6,0)"><g data-mml-node="mi"><use data-c="1D40C" xlink:href="#MJX-1016-TEX-B-1D40C"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(1092,0)"></use></g></g><g data-mml-node="mtext" transform="translate(4815.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5065.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(5343.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5593.6,0)"><g data-mml-node="mi"><use data-c="1D40C" xlink:href="#MJX-1016-TEX-B-1D40C"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(1092,0)"></use><use data-c="1D41A" xlink:href="#MJX-1016-TEX-B-1D41A" transform="translate(1619,0)"></use><use data-c="1D42C" xlink:href="#MJX-1016-TEX-B-1D42C" transform="translate(2178,0)"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(2632,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(3271,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(3745,0)"></use></g></g><g data-mml-node="mtext" transform="translate(9865.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-7718.2)"><g data-mml-node="mtd" transform="translate(4526.3,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g><g data-mml-node="mtext" transform="translate(278,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(528,0)"><g data-mml-node="mi"><use data-c="1D40B" xlink:href="#MJX-1016-TEX-B-1D40B"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(692,0)"></use><use data-c="1D41B" xlink:href="#MJX-1016-TEX-B-1D41B" transform="translate(1219,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(1858,0)"></use><use data-c="1D42C" xlink:href="#MJX-1016-TEX-B-1D42C" transform="translate(2385,0)"></use><use data-c="1D420" xlink:href="#MJX-1016-TEX-B-1D420" transform="translate(2839,0)"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(3414,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(4053,0)"></use></g></g><g data-mml-node="mtext" transform="translate(5108,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5358,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(5636,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5886,0)"><g data-mml-node="mi"><use data-c="1D401" xlink:href="#MJX-1016-TEX-B-1D401"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(818,0)"></use><use data-c="1D41C" xlink:href="#MJX-1016-TEX-B-1D41C" transform="translate(1393,0)"></use><use data-c="1D421" xlink:href="#MJX-1016-TEX-B-1D421" transform="translate(1904,0)"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(2543,0)"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(3182,0)"></use><use data-c="1D42B" xlink:href="#MJX-1016-TEX-B-1D42B" transform="translate(3709,0)"></use></g></g><g data-mml-node="mtext" transform="translate(10069,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-9118.2)"><g data-mml-node="mtd" transform="translate(4500.5,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="4C" xlink:href="#MJX-1016-TEX-N-4C"></use><use data-c="69" xlink:href="#MJX-1016-TEX-N-69" transform="translate(625,0)"></use><use data-c="6D" xlink:href="#MJX-1016-TEX-N-6D" transform="translate(903,0)"></use></g></g><g data-mml-node="mo" transform="translate(2013.8,0)"><g data-mml-node="text"><use data-c="3A" xlink:href="#MJX-1016-TEX-N-3A"></use></g><g data-mml-node="text" transform="translate(278,0)"><use data-c="3D" xlink:href="#MJX-1016-TEX-N-3D"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3347.6,0)"><g data-mml-node="mi"><use data-c="1D412" xlink:href="#MJX-1016-TEX-B-1D412"></use><use data-c="1D41E" xlink:href="#MJX-1016-TEX-B-1D41E" transform="translate(639,0)"></use><use data-c="1D42A" xlink:href="#MJX-1016-TEX-B-1D42A" transform="translate(1166,0)"></use></g></g><g data-mml-node="mtext" transform="translate(5120.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5370.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(5648.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(5898.6,0)"><g data-mml-node="mi"><use data-c="1D412" xlink:href="#MJX-1016-TEX-B-1D412"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(639,0)"></use><use data-c="1D429" xlink:href="#MJX-1016-TEX-B-1D429" transform="translate(1278,0)"></use></g></g><g data-mml-node="mtext" transform="translate(7815.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8065.6,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(8343.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(8593.6,0)"><g data-mml-node="mi"><use data-c="1D408" xlink:href="#MJX-1016-TEX-B-1D408"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(436,0)"></use><use data-c="1D41F" xlink:href="#MJX-1016-TEX-B-1D41F" transform="translate(1075,0)"></use></g></g><g data-mml-node="mtext" transform="translate(10120.6,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-10518.2)"><g data-mml-node="mtd" transform="translate(4504.8,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g><g data-mml-node="mtext" transform="translate(278,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(528,0)"><g data-mml-node="mi"><use data-c="1D40B" xlink:href="#MJX-1016-TEX-B-1D40B"></use><use data-c="1D422" xlink:href="#MJX-1016-TEX-B-1D422" transform="translate(692,0)"></use><use data-c="1D426" xlink:href="#MJX-1016-TEX-B-1D426" transform="translate(1011,0)"></use><use data-c="1D422" xlink:href="#MJX-1016-TEX-B-1D422" transform="translate(1969,0)"></use><use data-c="1D42D" xlink:href="#MJX-1016-TEX-B-1D42D" transform="translate(2288,0)"></use></g></g><g data-mml-node="mtext" transform="translate(3263,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(3513,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(3791,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(4041,0)"><g data-mml-node="mi"><use data-c="1D412" xlink:href="#MJX-1016-TEX-B-1D412"></use><use data-c="1D42E" xlink:href="#MJX-1016-TEX-B-1D42E" transform="translate(639,0)"></use><use data-c="1D426" xlink:href="#MJX-1016-TEX-B-1D426" transform="translate(1278,0)"></use></g></g><g data-mml-node="mtext" transform="translate(6277,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(6527,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1016-TEX-N-7C"></use></g></g><g data-mml-node="mtext" transform="translate(6805,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(7055,0)"><g data-mml-node="mi"><use data-c="1D414" xlink:href="#MJX-1016-TEX-B-1D414"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(885,0)"></use><use data-c="1D422" xlink:href="#MJX-1016-TEX-B-1D422" transform="translate(1524,0)"></use><use data-c="1D428" xlink:href="#MJX-1016-TEX-B-1D428" transform="translate(1843,0)"></use><use data-c="1D427" xlink:href="#MJX-1016-TEX-B-1D427" transform="translate(2418,0)"></use></g></g><g data-mml-node="mtext" transform="translate(10112,0)"><use data-c="A0" xlink:href="#MJX-1016-TEX-N-A0"></use></g></g></g><g data-mml-node="mtr" transform="translate(0,-11918.2)"><g data-mml-node="mtd" transform="translate(9685.8,0)"></g></g></g></g></g></svg></mjx-container>
</p><h1>SEMANTICS</h1><br><h2>MLTT</h2><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="17.262ex" height="1.609ex" role="img" focusable="false" viewBox="0 -700 7630 711" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1017-TEX-B-1D403" d="M39 624V686H270H310H408Q500 686 545 680T638 649Q768 584 805 438Q817 388 817 338Q817 171 702 75Q628 17 515 2Q504 1 270 0H39V62H147V624H39ZM655 337Q655 370 655 390T650 442T639 494T616 540T580 580T526 607T451 623Q443 624 368 624H298V62H377H387H407Q445 62 472 65T540 83T606 129Q629 156 640 195T653 262T655 337Z"></path><path id="MJX-1017-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-1017-TEX-B-1D41F" d="M308 0Q290 3 172 3Q58 3 49 0H40V62H109V382H42V444H109V503L110 562L112 572Q127 625 178 658T316 699Q318 699 330 699T348 700Q381 698 404 687T436 658T449 629T452 606Q452 576 432 557T383 537Q355 537 335 555T314 605Q314 635 328 649H325Q311 649 293 644T253 618T227 560Q226 555 226 498V444H340V382H232V62H318V0H308Z"></path><path id="MJX-1017-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-1017-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1017-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-1017-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-1017-TEX-B-A0" d=""></path><path id="MJX-1017-TEX-B-1D7CF" d="M481 0L294 3Q136 3 109 0H96V62H227V304Q227 546 225 546Q169 529 97 529H80V591H97Q231 591 308 647L319 655H333Q355 655 359 644Q361 640 361 351V62H494V0H481Z"></path><path id="MJX-1017-TEX-B-2E" d="M74 85Q74 121 99 146T156 171Q200 171 222 143T245 85Q245 56 224 29T160 1Q118 1 96 27T74 85Z"></path><path id="MJX-1017-TEX-B-1D7D1" d="M80 503Q80 565 133 610T274 655Q366 655 421 623T491 538Q493 528 493 510Q493 446 453 407T361 348L376 344Q452 324 489 281T526 184Q526 152 514 121T474 58T392 8T265 -11Q175 -11 111 34T48 152Q50 187 72 209T132 232Q171 232 193 208T216 147Q216 136 214 126T207 108T197 94T187 84T178 77T170 72L168 71Q168 70 179 65T215 54T266 48H270Q331 48 350 105Q358 128 358 185Q358 239 348 268T309 313Q292 321 242 322Q205 322 198 324T191 341V348Q191 366 196 369T232 375Q239 375 247 376T260 377T268 378Q284 383 297 393T326 436T341 517Q341 536 339 547T331 573T308 593T266 600Q248 600 241 599Q214 593 183 576Q234 556 234 503Q234 462 210 444T157 426Q126 426 103 446T80 503Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D403" xlink:href="#MJX-1017-TEX-B-1D403"></use><use data-c="1D41E" xlink:href="#MJX-1017-TEX-B-1D41E" transform="translate(882,0)"></use><use data-c="1D41F" xlink:href="#MJX-1017-TEX-B-1D41F" transform="translate(1409,0)"></use><use data-c="1D422" xlink:href="#MJX-1017-TEX-B-1D422" transform="translate(1760,0)"></use><use data-c="1D427" xlink:href="#MJX-1017-TEX-B-1D427" transform="translate(2079,0)"></use><use data-c="1D422" xlink:href="#MJX-1017-TEX-B-1D422" transform="translate(2718,0)"></use><use data-c="1D42D" xlink:href="#MJX-1017-TEX-B-1D42D" transform="translate(3037,0)"></use><use data-c="1D422" xlink:href="#MJX-1017-TEX-B-1D422" transform="translate(3484,0)"></use><use data-c="1D428" xlink:href="#MJX-1017-TEX-B-1D428" transform="translate(3803,0)"></use><use data-c="1D427" xlink:href="#MJX-1017-TEX-B-1D427" transform="translate(4378,0)"></use></g><g data-mml-node="mtext" transform="translate(5017,0)"><use data-c="A0" xlink:href="#MJX-1017-TEX-B-A0"></use></g><g data-mml-node="mn" transform="translate(5267,0)"><use data-c="1D7CF" xlink:href="#MJX-1017-TEX-B-1D7CF"></use><use data-c="2E" xlink:href="#MJX-1017-TEX-B-2E" transform="translate(575,0)"></use><use data-c="1D7D1" xlink:href="#MJX-1017-TEX-B-1D7D1" transform="translate(894,0)"></use></g><g data-mml-node="mn" transform="translate(6736,0)"><use data-c="2E" xlink:href="#MJX-1017-TEX-B-2E"></use><use data-c="1D7CF" xlink:href="#MJX-1017-TEX-B-1D7CF" transform="translate(319,0)"></use></g></g></g></g></svg></mjx-container> (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.05ex;" xmlns="http://www.w3.org/2000/svg" width="1.258ex" height="1.62ex" role="img" focusable="false" viewBox="0 -694 556 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1018-TEX-N-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="2200" xlink:href="#MJX-1018-TEX-N-2200"></use></g></g></g></svg></mjx-container>-Formation, Dependent Product).
<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.05ex;" xmlns="http://www.w3.org/2000/svg" width="1.258ex" height="1.62ex" role="img" focusable="false" viewBox="0 -694 556 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1019-TEX-N-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="2200" xlink:href="#MJX-1019-TEX-N-2200"></use></g></g></g></svg></mjx-container>-types represents the way we create the spaces of dependent functions <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.566ex;" xmlns="http://www.w3.org/2000/svg" width="17.368ex" height="2.262ex" role="img" focusable="false" viewBox="0 -750 7676.8 1000" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1020-TEX-I-1D453" d="M118 -162Q120 -162 124 -164T135 -167T147 -168Q160 -168 171 -155T187 -126Q197 -99 221 27T267 267T289 382V385H242Q195 385 192 387Q188 390 188 397L195 425Q197 430 203 430T250 431Q298 431 298 432Q298 434 307 482T319 540Q356 705 465 705Q502 703 526 683T550 630Q550 594 529 578T487 561Q443 561 443 603Q443 622 454 636T478 657L487 662Q471 668 457 668Q445 668 434 658T419 630Q412 601 403 552T387 469T380 433Q380 431 435 431Q480 431 487 430T498 424Q499 420 496 407T491 391Q489 386 482 386T428 385H372L349 263Q301 15 282 -47Q255 -132 212 -173Q175 -205 139 -205Q107 -205 81 -186T55 -132Q55 -95 76 -78T118 -61Q162 -61 162 -103Q162 -122 151 -136T127 -157L118 -162Z"></path><path id="MJX-1020-TEX-N-3A" d="M78 370Q78 394 95 412T138 430Q162 430 180 414T199 371Q199 346 182 328T139 310T96 327T78 370ZM78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path id="MJX-1020-TEX-N-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path><path id="MJX-1020-TEX-N-A0" d=""></path><path id="MJX-1020-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-1020-TEX-I-1D465" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path id="MJX-1020-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path><path id="MJX-1020-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path id="MJX-1020-TEX-N-2C" d="M78 35T78 60T94 103T137 121Q165 121 187 96T210 8Q210 -27 201 -60T180 -117T154 -158T130 -185T117 -194Q113 -194 104 -185T95 -172Q95 -168 106 -156T131 -126T157 -76T173 -3V9L172 8Q170 7 167 6T161 3T152 1T140 0Q113 0 96 17Z"></path><path id="MJX-1020-TEX-I-1D435" d="M231 637Q204 637 199 638T194 649Q194 676 205 682Q206 683 335 683Q594 683 608 681Q671 671 713 636T756 544Q756 480 698 429T565 360L555 357Q619 348 660 311T702 219Q702 146 630 78T453 1Q446 0 242 0Q42 0 39 2Q35 5 35 10Q35 17 37 24Q42 43 47 45Q51 46 62 46H68Q95 46 128 49Q142 52 147 61Q150 65 219 339T288 628Q288 635 231 637ZM649 544Q649 574 634 600T585 634Q578 636 493 637Q473 637 451 637T416 636H403Q388 635 384 626Q382 622 352 506Q352 503 351 500L320 374H401Q482 374 494 376Q554 386 601 434T649 544ZM595 229Q595 273 572 302T512 336Q506 337 429 337Q311 337 310 336Q310 334 293 263T258 122L240 52Q240 48 252 48T333 46Q422 46 429 47Q491 54 543 105T595 229Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D453" xlink:href="#MJX-1020-TEX-I-1D453"></use></g><g data-mml-node="mo" transform="translate(827.8,0)"><use data-c="3A" xlink:href="#MJX-1020-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(1383.6,0)"><use data-c="2200" xlink:href="#MJX-1020-TEX-N-2200"></use></g><g data-mml-node="mtext" transform="translate(1939.6,0)"><use data-c="A0" xlink:href="#MJX-1020-TEX-N-A0"></use></g><g data-mml-node="mo" transform="translate(2189.6,0)"><use data-c="28" xlink:href="#MJX-1020-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(2578.6,0)"><use data-c="1D465" xlink:href="#MJX-1020-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(3428.3,0)"><use data-c="3A" xlink:href="#MJX-1020-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(3984.1,0)"><use data-c="1D434" xlink:href="#MJX-1020-TEX-I-1D434"></use></g><g data-mml-node="mo" transform="translate(4734.1,0)"><use data-c="29" xlink:href="#MJX-1020-TEX-N-29"></use></g><g data-mml-node="mo" transform="translate(5123.1,0)"><use data-c="2C" xlink:href="#MJX-1020-TEX-N-2C"></use></g><g data-mml-node="mi" transform="translate(5567.8,0)"><use data-c="1D435" xlink:href="#MJX-1020-TEX-I-1D435"></use></g><g data-mml-node="mo" transform="translate(6326.8,0)"><use data-c="28" xlink:href="#MJX-1020-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(6715.8,0)"><use data-c="1D465" xlink:href="#MJX-1020-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(7287.8,0)"><use data-c="29" xlink:href="#MJX-1020-TEX-N-29"></use></g></g></g></svg></mjx-container>
with domain in <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.697ex" height="1.62ex" role="img" focusable="false" viewBox="0 -716 750 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1021-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-1021-TEX-I-1D434"></use></g></g></g></svg></mjx-container> and codomain in type family <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.05ex;" xmlns="http://www.w3.org/2000/svg" width="10.555ex" height="1.67ex" role="img" focusable="false" viewBox="0 -716 4665.1 738" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1022-TEX-I-1D435" d="M231 637Q204 637 199 638T194 649Q194 676 205 682Q206 683 335 683Q594 683 608 681Q671 671 713 636T756 544Q756 480 698 429T565 360L555 357Q619 348 660 311T702 219Q702 146 630 78T453 1Q446 0 242 0Q42 0 39 2Q35 5 35 10Q35 17 37 24Q42 43 47 45Q51 46 62 46H68Q95 46 128 49Q142 52 147 61Q150 65 219 339T288 628Q288 635 231 637ZM649 544Q649 574 634 600T585 634Q578 636 493 637Q473 637 451 637T416 636H403Q388 635 384 626Q382 622 352 506Q352 503 351 500L320 374H401Q482 374 494 376Q554 386 601 434T649 544ZM595 229Q595 273 572 302T512 336Q506 337 429 337Q311 337 310 336Q310 334 293 263T258 122L240 52Q240 48 252 48T333 46Q422 46 429 47Q491 54 543 105T595 229Z"></path><path id="MJX-1022-TEX-N-3A" d="M78 370Q78 394 95 412T138 430Q162 430 180 414T199 371Q199 346 182 328T139 310T96 327T78 370ZM78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path id="MJX-1022-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path><path id="MJX-1022-TEX-N-2192" d="M56 237T56 250T70 270H835Q719 357 692 493Q692 494 692 496T691 499Q691 511 708 511H711Q720 511 723 510T729 506T732 497T735 481T743 456Q765 389 816 336T935 261Q944 258 944 250Q944 244 939 241T915 231T877 212Q836 186 806 152T761 85T740 35T732 4Q730 -6 727 -8T711 -11Q691 -11 691 0Q691 7 696 25Q728 151 835 230H70Q56 237 56 250Z"></path><path id="MJX-1022-TEX-I-1D448" d="M107 637Q73 637 71 641Q70 643 70 649Q70 673 81 682Q83 683 98 683Q139 681 234 681Q268 681 297 681T342 682T362 682Q378 682 378 672Q378 670 376 658Q371 641 366 638H364Q362 638 359 638T352 638T343 637T334 637Q295 636 284 634T266 623Q265 621 238 518T184 302T154 169Q152 155 152 140Q152 86 183 55T269 24Q336 24 403 69T501 205L552 406Q599 598 599 606Q599 633 535 637Q511 637 511 648Q511 650 513 660Q517 676 519 679T529 683Q532 683 561 682T645 680Q696 680 723 681T752 682Q767 682 767 672Q767 650 759 642Q756 637 737 637Q666 633 648 597Q646 592 598 404Q557 235 548 205Q515 105 433 42T263 -22Q171 -22 116 34T60 167V183Q60 201 115 421Q164 622 164 628Q164 635 107 637Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D435" xlink:href="#MJX-1022-TEX-I-1D435"></use></g><g data-mml-node="mo" transform="translate(1036.8,0)"><use data-c="3A" xlink:href="#MJX-1022-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(1592.6,0)"><use data-c="1D434" xlink:href="#MJX-1022-TEX-I-1D434"></use></g><g data-mml-node="mo" transform="translate(2620.3,0)"><use data-c="2192" xlink:href="#MJX-1022-TEX-N-2192"></use></g><g data-mml-node="mi" transform="translate(3898.1,0)"><use data-c="1D448" xlink:href="#MJX-1022-TEX-I-1D448"></use></g></g></g></svg></mjx-container> over <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.697ex" height="1.62ex" role="img" focusable="false" viewBox="0 -716 750 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1023-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-1023-TEX-I-1D434"></use></g></g></g></svg></mjx-container>.</p><p style="text-align:center;"><mjx-container class="MathJax" jax="SVG" display="true"><svg style="vertical-align: -2.803ex;" xmlns="http://www.w3.org/2000/svg" width="23.276ex" height="4.952ex" role="img" focusable="false" viewBox="0 -950 10288.1 2188.8" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1024-TEX-N-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path><path id="MJX-1024-TEX-N-3A" d="M78 370Q78 394 95 412T138 430Q162 430 180 414T199 371Q199 346 182 328T139 310T96 327T78 370ZM78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path id="MJX-1024-TEX-I-1D448" d="M107 637Q73 637 71 641Q70 643 70 649Q70 673 81 682Q83 683 98 683Q139 681 234 681Q268 681 297 681T342 682T362 682Q378 682 378 672Q378 670 376 658Q371 641 366 638H364Q362 638 359 638T352 638T343 637T334 637Q295 636 284 634T266 623Q265 621 238 518T184 302T154 169Q152 155 152 140Q152 86 183 55T269 24Q336 24 403 69T501 205L552 406Q599 598 599 606Q599 633 535 637Q511 637 511 648Q511 650 513 660Q517 676 519 679T529 683Q532 683 561 682T645 680Q696 680 723 681T752 682Q767 682 767 672Q767 650 759 642Q756 637 737 637Q666 633 648 597Q646 592 598 404Q557 235 548 205Q515 105 433 42T263 -22Q171 -22 116 34T60 167V183Q60 201 115 421Q164 622 164 628Q164 635 107 637Z"></path><path id="MJX-1024-TEX-N-30" d="M96 585Q152 666 249 666Q297 666 345 640T423 548Q460 465 460 320Q460 165 417 83Q397 41 362 16T301 -15T250 -22Q224 -22 198 -16T137 16T82 83Q39 165 39 320Q39 494 96 585ZM321 597Q291 629 250 629Q208 629 178 597Q153 571 145 525T137 333Q137 175 145 125T181 46Q209 16 250 16Q290 16 318 46Q347 76 354 130T362 333Q362 478 354 524T321 597Z"></path><path id="MJX-1024-TEX-N-3D" d="M56 347Q56 360 70 367H707Q722 359 722 347Q722 336 708 328L390 327H72Q56 332 56 347ZM56 153Q56 168 72 173H708Q722 163 722 153Q722 140 707 133H70Q56 140 56 153Z"></path><path id="MJX-1024-TEX-I-1D451" d="M366 683Q367 683 438 688T511 694Q523 694 523 686Q523 679 450 384T375 83T374 68Q374 26 402 26Q411 27 422 35Q443 55 463 131Q469 151 473 152Q475 153 483 153H487H491Q506 153 506 145Q506 140 503 129Q490 79 473 48T445 8T417 -8Q409 -10 393 -10Q359 -10 336 5T306 36L300 51Q299 52 296 50Q294 48 292 46Q233 -10 172 -10Q117 -10 75 30T33 157Q33 205 53 255T101 341Q148 398 195 420T280 442Q336 442 364 400Q369 394 369 396Q370 400 396 505T424 616Q424 629 417 632T378 637H357Q351 643 351 645T353 664Q358 683 366 683ZM352 326Q329 405 277 405Q242 405 210 374T160 293Q131 214 119 129Q119 126 119 118T118 106Q118 61 136 44T179 26Q233 26 290 98L298 109L352 326Z"></path><path id="MJX-1024-TEX-I-1D452" d="M39 168Q39 225 58 272T107 350T174 402T244 433T307 442H310Q355 442 388 420T421 355Q421 265 310 237Q261 224 176 223Q139 223 138 221Q138 219 132 186T125 128Q125 81 146 54T209 26T302 45T394 111Q403 121 406 121Q410 121 419 112T429 98T420 82T390 55T344 24T281 -1T205 -11Q126 -11 83 42T39 168ZM373 353Q367 405 305 405Q272 405 244 391T199 357T170 316T154 280T149 261Q149 260 169 260Q282 260 327 284T373 353Z"></path><path id="MJX-1024-TEX-I-1D453" d="M118 -162Q120 -162 124 -164T135 -167T147 -168Q160 -168 171 -155T187 -126Q197 -99 221 27T267 267T289 382V385H242Q195 385 192 387Q188 390 188 397L195 425Q197 430 203 430T250 431Q298 431 298 432Q298 434 307 482T319 540Q356 705 465 705Q502 703 526 683T550 630Q550 594 529 578T487 561Q443 561 443 603Q443 622 454 636T478 657L487 662Q471 668 457 668Q445 668 434 658T419 630Q412 601 403 552T387 469T380 433Q380 431 435 431Q480 431 487 430T498 424Q499 420 496 407T491 391Q489 386 482 386T428 385H372L349 263Q301 15 282 -47Q255 -132 212 -173Q175 -205 139 -205Q107 -205 81 -186T55 -132Q55 -95 76 -78T118 -61Q162 -61 162 -103Q162 -122 151 -136T127 -157L118 -162Z"></path><path id="MJX-1024-TEX-LO-220F" d="M220 812Q220 813 218 819T214 829T208 840T199 853T185 866T166 878T140 887T107 893T66 896H56V950H1221V896H1211Q1080 896 1058 812V-311Q1076 -396 1211 -396H1221V-450H725V-396H735Q864 -396 888 -314Q889 -312 889 -311V896H388V292L389 -311Q405 -396 542 -396H552V-450H56V-396H66Q195 -396 219 -314Q220 -312 220 -311V812Z"></path><path id="MJX-1024-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path><path id="MJX-1024-TEX-I-1D465" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path id="MJX-1024-TEX-I-1D435" d="M231 637Q204 637 199 638T194 649Q194 676 205 682Q206 683 335 683Q594 683 608 681Q671 671 713 636T756 544Q756 480 698 429T565 360L555 357Q619 348 660 311T702 219Q702 146 630 78T453 1Q446 0 242 0Q42 0 39 2Q35 5 35 10Q35 17 37 24Q42 43 47 45Q51 46 62 46H68Q95 46 128 49Q142 52 147 61Q150 65 219 339T288 628Q288 635 231 637ZM649 544Q649 574 634 600T585 634Q578 636 493 637Q473 637 451 637T416 636H403Q388 635 384 626Q382 622 352 506Q352 503 351 500L320 374H401Q482 374 494 376Q554 386 601 434T649 544ZM595 229Q595 273 572 302T512 336Q506 337 429 337Q311 337 310 336Q310 334 293 263T258 122L240 52Q240 48 252 48T333 46Q422 46 429 47Q491 54 543 105T595 229Z"></path><path id="MJX-1024-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-1024-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path id="MJX-1024-TEX-N-2E" d="M78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="2200" xlink:href="#MJX-1024-TEX-N-2200"></use></g><g data-mml-node="mo" transform="translate(833.8,0)"><use data-c="3A" xlink:href="#MJX-1024-TEX-N-3A"></use></g><g data-mml-node="msub" transform="translate(1389.6,0)"><g data-mml-node="mi"><use data-c="1D448" xlink:href="#MJX-1024-TEX-I-1D448"></use></g><g data-mml-node="mn" transform="translate(716,-150) scale(0.707)"><use data-c="30" xlink:href="#MJX-1024-TEX-N-30"></use></g></g><g data-mml-node="msub" transform="translate(2786.9,0)"><g data-mml-node="mo"><use data-c="3D" xlink:href="#MJX-1024-TEX-N-3D"></use></g><g data-mml-node="TeXAtom" transform="translate(811,-150) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D451" xlink:href="#MJX-1024-TEX-I-1D451"></use></g><g data-mml-node="mi" transform="translate(520,0)"><use data-c="1D452" xlink:href="#MJX-1024-TEX-I-1D452"></use></g><g data-mml-node="mi" transform="translate(986,0)"><use data-c="1D453" xlink:href="#MJX-1024-TEX-I-1D453"></use></g></g></g><g data-mml-node="munder" transform="translate(5011.8,0)"><g data-mml-node="mo"><use data-c="220F" xlink:href="#MJX-1024-TEX-LO-220F"></use></g><g data-mml-node="TeXAtom" transform="translate(4.4,-1123.3) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-1024-TEX-I-1D434"></use></g><g data-mml-node="mo" transform="translate(750,0)"><use data-c="3A" xlink:href="#MJX-1024-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(1028,0)"><use data-c="1D448" xlink:href="#MJX-1024-TEX-I-1D448"></use></g></g></g><g data-mml-node="munder" transform="translate(6456.4,0)"><g data-mml-node="mo"><use data-c="220F" xlink:href="#MJX-1024-TEX-LO-220F"></use></g><g data-mml-node="TeXAtom" transform="translate(73.3,-1123.3) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D465" xlink:href="#MJX-1024-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(572,0)"><use data-c="3A" xlink:href="#MJX-1024-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(850,0)"><use data-c="1D434" xlink:href="#MJX-1024-TEX-I-1D434"></use></g></g></g><g data-mml-node="mi" transform="translate(7901.1,0)"><use data-c="1D435" xlink:href="#MJX-1024-TEX-I-1D435"></use></g><g data-mml-node="mo" transform="translate(8660.1,0)"><use data-c="28" xlink:href="#MJX-1024-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(9049.1,0)"><use data-c="1D465" xlink:href="#MJX-1024-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(9621.1,0)"><use data-c="29" xlink:href="#MJX-1024-TEX-N-29"></use></g><g data-mml-node="mo" transform="translate(10010.1,0)"><use data-c="2E" xlink:href="#MJX-1024-TEX-N-2E"></use></g></g></g></svg></mjx-container>
</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="17.262ex" height="1.597ex" role="img" focusable="false" viewBox="0 -700 7630 706" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1025-TEX-B-1D403" d="M39 624V686H270H310H408Q500 686 545 680T638 649Q768 584 805 438Q817 388 817 338Q817 171 702 75Q628 17 515 2Q504 1 270 0H39V62H147V624H39ZM655 337Q655 370 655 390T650 442T639 494T616 540T580 580T526 607T451 623Q443 624 368 624H298V62H377H387H407Q445 62 472 65T540 83T606 129Q629 156 640 195T653 262T655 337Z"></path><path id="MJX-1025-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-1025-TEX-B-1D41F" d="M308 0Q290 3 172 3Q58 3 49 0H40V62H109V382H42V444H109V503L110 562L112 572Q127 625 178 658T316 699Q318 699 330 699T348 700Q381 698 404 687T436 658T449 629T452 606Q452 576 432 557T383 537Q355 537 335 555T314 605Q314 635 328 649H325Q311 649 293 644T253 618T227 560Q226 555 226 498V444H340V382H232V62H318V0H308Z"></path><path id="MJX-1025-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-1025-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1025-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-1025-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-1025-TEX-B-A0" d=""></path><path id="MJX-1025-TEX-B-1D7CF" d="M481 0L294 3Q136 3 109 0H96V62H227V304Q227 546 225 546Q169 529 97 529H80V591H97Q231 591 308 647L319 655H333Q355 655 359 644Q361 640 361 351V62H494V0H481Z"></path><path id="MJX-1025-TEX-B-2E" d="M74 85Q74 121 99 146T156 171Q200 171 222 143T245 85Q245 56 224 29T160 1Q118 1 96 27T74 85Z"></path><path id="MJX-1025-TEX-B-1D7D2" d="M531 0Q510 3 381 3Q238 3 214 0H201V62H313V155H32V217L205 434Q342 606 362 630T387 655L391 656Q395 656 401 656T414 656H427Q447 656 451 645Q453 641 453 429V217H542V155H453V62H542V0H531ZM324 217V494L103 218L213 217H324Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D403" xlink:href="#MJX-1025-TEX-B-1D403"></use><use data-c="1D41E" xlink:href="#MJX-1025-TEX-B-1D41E" transform="translate(882,0)"></use><use data-c="1D41F" xlink:href="#MJX-1025-TEX-B-1D41F" transform="translate(1409,0)"></use><use data-c="1D422" xlink:href="#MJX-1025-TEX-B-1D422" transform="translate(1760,0)"></use><use data-c="1D427" xlink:href="#MJX-1025-TEX-B-1D427" transform="translate(2079,0)"></use><use data-c="1D422" xlink:href="#MJX-1025-TEX-B-1D422" transform="translate(2718,0)"></use><use data-c="1D42D" xlink:href="#MJX-1025-TEX-B-1D42D" transform="translate(3037,0)"></use><use data-c="1D422" xlink:href="#MJX-1025-TEX-B-1D422" transform="translate(3484,0)"></use><use data-c="1D428" xlink:href="#MJX-1025-TEX-B-1D428" transform="translate(3803,0)"></use><use data-c="1D427" xlink:href="#MJX-1025-TEX-B-1D427" transform="translate(4378,0)"></use></g><g data-mml-node="mtext" transform="translate(5017,0)"><use data-c="A0" xlink:href="#MJX-1025-TEX-B-A0"></use></g><g data-mml-node="mn" transform="translate(5267,0)"><use data-c="1D7CF" xlink:href="#MJX-1025-TEX-B-1D7CF"></use><use data-c="2E" xlink:href="#MJX-1025-TEX-B-2E" transform="translate(575,0)"></use><use data-c="1D7D2" xlink:href="#MJX-1025-TEX-B-1D7D2" transform="translate(894,0)"></use></g><g data-mml-node="mn" transform="translate(6736,0)"><use data-c="2E" xlink:href="#MJX-1025-TEX-B-2E"></use><use data-c="1D7CF" xlink:href="#MJX-1025-TEX-B-1D7CF" transform="translate(319,0)"></use></g></g></g></g></svg></mjx-container> (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.258ex" height="1.57ex" role="img" focusable="false" viewBox="0 -694 556 694" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1026-TEX-N-2203" d="M56 661T56 674T70 694H487Q497 686 500 679V15Q497 10 487 1L279 0H70Q56 7 56 20T70 40H460V327H84Q70 334 70 347T84 367H460V654H70Q56 661 56 674Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="2203" xlink:href="#MJX-1026-TEX-N-2203"></use></g></g></g></svg></mjx-container>-Formation, Dependent Sum). The dependent sum
type is indexed over type <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.697ex" height="1.62ex" role="img" focusable="false" viewBox="0 -716 750 716" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1027-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-1027-TEX-I-1D434"></use></g></g></g></svg></mjx-container> in the sense of coproduct or disjoint union,
where only one fiber codomain <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.566ex;" xmlns="http://www.w3.org/2000/svg" width="4.771ex" height="2.262ex" role="img" focusable="false" viewBox="0 -750 2109 1000" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1028-TEX-I-1D435" d="M231 637Q204 637 199 638T194 649Q194 676 205 682Q206 683 335 683Q594 683 608 681Q671 671 713 636T756 544Q756 480 698 429T565 360L555 357Q619 348 660 311T702 219Q702 146 630 78T453 1Q446 0 242 0Q42 0 39 2Q35 5 35 10Q35 17 37 24Q42 43 47 45Q51 46 62 46H68Q95 46 128 49Q142 52 147 61Q150 65 219 339T288 628Q288 635 231 637ZM649 544Q649 574 634 600T585 634Q578 636 493 637Q473 637 451 637T416 636H403Q388 635 384 626Q382 622 352 506Q352 503 351 500L320 374H401Q482 374 494 376Q554 386 601 434T649 544ZM595 229Q595 273 572 302T512 336Q506 337 429 337Q311 337 310 336Q310 334 293 263T258 122L240 52Q240 48 252 48T333 46Q422 46 429 47Q491 54 543 105T595 229Z"></path><path id="MJX-1028-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-1028-TEX-I-1D465" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path id="MJX-1028-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="1D435" xlink:href="#MJX-1028-TEX-I-1D435"></use></g><g data-mml-node="mo" transform="translate(759,0)"><use data-c="28" xlink:href="#MJX-1028-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(1148,0)"><use data-c="1D465" xlink:href="#MJX-1028-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(1720,0)"><use data-c="29" xlink:href="#MJX-1028-TEX-N-29"></use></g></g></g></svg></mjx-container> is present in pair.</p><p style="text-align:center;"><mjx-container class="MathJax" jax="SVG" display="true"><svg style="vertical-align: -2.803ex;" xmlns="http://www.w3.org/2000/svg" width="29.954ex" height="4.952ex" role="img" focusable="false" viewBox="0 -950 13239.8 2188.8" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1029-TEX-N-2203" d="M56 661T56 674T70 694H487Q497 686 500 679V15Q497 10 487 1L279 0H70Q56 7 56 20T70 40H460V327H84Q70 334 70 347T84 367H460V654H70Q56 661 56 674Z"></path><path id="MJX-1029-TEX-N-3A" d="M78 370Q78 394 95 412T138 430Q162 430 180 414T199 371Q199 346 182 328T139 310T96 327T78 370ZM78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path id="MJX-1029-TEX-I-1D443" d="M287 628Q287 635 230 637Q206 637 199 638T192 648Q192 649 194 659Q200 679 203 681T397 683Q587 682 600 680Q664 669 707 631T751 530Q751 453 685 389Q616 321 507 303Q500 302 402 301H307L277 182Q247 66 247 59Q247 55 248 54T255 50T272 48T305 46H336Q342 37 342 35Q342 19 335 5Q330 0 319 0Q316 0 282 1T182 2Q120 2 87 2T51 1Q33 1 33 11Q33 13 36 25Q40 41 44 43T67 46Q94 46 127 49Q141 52 146 61Q149 65 218 339T287 628ZM645 554Q645 567 643 575T634 597T609 619T560 635Q553 636 480 637Q463 637 445 637T416 636T404 636Q391 635 386 627Q384 621 367 550T332 412T314 344Q314 342 395 342H407H430Q542 342 590 392Q617 419 631 471T645 554Z"></path><path id="MJX-1029-TEX-I-1D45F" d="M21 287Q22 290 23 295T28 317T38 348T53 381T73 411T99 433T132 442Q161 442 183 430T214 408T225 388Q227 382 228 382T236 389Q284 441 347 441H350Q398 441 422 400Q430 381 430 363Q430 333 417 315T391 292T366 288Q346 288 334 299T322 328Q322 376 378 392Q356 405 342 405Q286 405 239 331Q229 315 224 298T190 165Q156 25 151 16Q138 -11 108 -11Q95 -11 87 -5T76 7T74 17Q74 30 114 189T154 366Q154 405 128 405Q107 405 92 377T68 316T57 280Q55 278 41 278H27Q21 284 21 287Z"></path><path id="MJX-1029-TEX-I-1D45C" d="M201 -11Q126 -11 80 38T34 156Q34 221 64 279T146 380Q222 441 301 441Q333 441 341 440Q354 437 367 433T402 417T438 387T464 338T476 268Q476 161 390 75T201 -11ZM121 120Q121 70 147 48T206 26Q250 26 289 58T351 142Q360 163 374 216T388 308Q388 352 370 375Q346 405 306 405Q243 405 195 347Q158 303 140 230T121 120Z"></path><path id="MJX-1029-TEX-I-1D45D" d="M23 287Q24 290 25 295T30 317T40 348T55 381T75 411T101 433T134 442Q209 442 230 378L240 387Q302 442 358 442Q423 442 460 395T497 281Q497 173 421 82T249 -10Q227 -10 210 -4Q199 1 187 11T168 28L161 36Q160 35 139 -51T118 -138Q118 -144 126 -145T163 -148H188Q194 -155 194 -157T191 -175Q188 -187 185 -190T172 -194Q170 -194 161 -194T127 -193T65 -192Q-5 -192 -24 -194H-32Q-39 -187 -39 -183Q-37 -156 -26 -148H-6Q28 -147 33 -136Q36 -130 94 103T155 350Q156 355 156 364Q156 405 131 405Q109 405 94 377T71 316T59 280Q57 278 43 278H29Q23 284 23 287ZM178 102Q200 26 252 26Q282 26 310 49T356 107Q374 141 392 215T411 325V331Q411 405 350 405Q339 405 328 402T306 393T286 380T269 365T254 350T243 336T235 326L232 322Q232 321 229 308T218 264T204 212Q178 106 178 102Z"></path><path id="MJX-1029-TEX-N-3D" d="M56 347Q56 360 70 367H707Q722 359 722 347Q722 336 708 328L390 327H72Q56 332 56 347ZM56 153Q56 168 72 173H708Q722 163 722 153Q722 140 707 133H70Q56 140 56 153Z"></path><path id="MJX-1029-TEX-I-1D451" d="M366 683Q367 683 438 688T511 694Q523 694 523 686Q523 679 450 384T375 83T374 68Q374 26 402 26Q411 27 422 35Q443 55 463 131Q469 151 473 152Q475 153 483 153H487H491Q506 153 506 145Q506 140 503 129Q490 79 473 48T445 8T417 -8Q409 -10 393 -10Q359 -10 336 5T306 36L300 51Q299 52 296 50Q294 48 292 46Q233 -10 172 -10Q117 -10 75 30T33 157Q33 205 53 255T101 341Q148 398 195 420T280 442Q336 442 364 400Q369 394 369 396Q370 400 396 505T424 616Q424 629 417 632T378 637H357Q351 643 351 645T353 664Q358 683 366 683ZM352 326Q329 405 277 405Q242 405 210 374T160 293Q131 214 119 129Q119 126 119 118T118 106Q118 61 136 44T179 26Q233 26 290 98L298 109L352 326Z"></path><path id="MJX-1029-TEX-I-1D452" d="M39 168Q39 225 58 272T107 350T174 402T244 433T307 442H310Q355 442 388 420T421 355Q421 265 310 237Q261 224 176 223Q139 223 138 221Q138 219 132 186T125 128Q125 81 146 54T209 26T302 45T394 111Q403 121 406 121Q410 121 419 112T429 98T420 82T390 55T344 24T281 -1T205 -11Q126 -11 83 42T39 168ZM373 353Q367 405 305 405Q272 405 244 391T199 357T170 316T154 280T149 261Q149 260 169 260Q282 260 327 284T373 353Z"></path><path id="MJX-1029-TEX-I-1D453" d="M118 -162Q120 -162 124 -164T135 -167T147 -168Q160 -168 171 -155T187 -126Q197 -99 221 27T267 267T289 382V385H242Q195 385 192 387Q188 390 188 397L195 425Q197 430 203 430T250 431Q298 431 298 432Q298 434 307 482T319 540Q356 705 465 705Q502 703 526 683T550 630Q550 594 529 578T487 561Q443 561 443 603Q443 622 454 636T478 657L487 662Q471 668 457 668Q445 668 434 658T419 630Q412 601 403 552T387 469T380 433Q380 431 435 431Q480 431 487 430T498 424Q499 420 496 407T491 391Q489 386 482 386T428 385H372L349 263Q301 15 282 -47Q255 -132 212 -173Q175 -205 139 -205Q107 -205 81 -186T55 -132Q55 -95 76 -78T118 -61Q162 -61 162 -103Q162 -122 151 -136T127 -157L118 -162Z"></path><path id="MJX-1029-TEX-N-7C" d="M139 -249H137Q125 -249 119 -235V251L120 737Q130 750 139 750Q152 750 159 735V-235Q151 -249 141 -249H139Z"></path><path id="MJX-1029-TEX-LO-220F" d="M220 812Q220 813 218 819T214 829T208 840T199 853T185 866T166 878T140 887T107 893T66 896H56V950H1221V896H1211Q1080 896 1058 812V-311Q1076 -396 1211 -396H1221V-450H725V-396H735Q864 -396 888 -314Q889 -312 889 -311V896H388V292L389 -311Q405 -396 542 -396H552V-450H56V-396H66Q195 -396 219 -314Q220 -312 220 -311V812Z"></path><path id="MJX-1029-TEX-I-1D434" d="M208 74Q208 50 254 46Q272 46 272 35Q272 34 270 22Q267 8 264 4T251 0Q249 0 239 0T205 1T141 2Q70 2 50 0H42Q35 7 35 11Q37 38 48 46H62Q132 49 164 96Q170 102 345 401T523 704Q530 716 547 716H555H572Q578 707 578 706L606 383Q634 60 636 57Q641 46 701 46Q726 46 726 36Q726 34 723 22Q720 7 718 4T704 0Q701 0 690 0T651 1T578 2Q484 2 455 0H443Q437 6 437 9T439 27Q443 40 445 43L449 46H469Q523 49 533 63L521 213H283L249 155Q208 86 208 74ZM516 260Q516 271 504 416T490 562L463 519Q447 492 400 412L310 260L413 259Q516 259 516 260Z"></path><path id="MJX-1029-TEX-I-1D448" d="M107 637Q73 637 71 641Q70 643 70 649Q70 673 81 682Q83 683 98 683Q139 681 234 681Q268 681 297 681T342 682T362 682Q378 682 378 672Q378 670 376 658Q371 641 366 638H364Q362 638 359 638T352 638T343 637T334 637Q295 636 284 634T266 623Q265 621 238 518T184 302T154 169Q152 155 152 140Q152 86 183 55T269 24Q336 24 403 69T501 205L552 406Q599 598 599 606Q599 633 535 637Q511 637 511 648Q511 650 513 660Q517 676 519 679T529 683Q532 683 561 682T645 680Q696 680 723 681T752 682Q767 682 767 672Q767 650 759 642Q756 637 737 637Q666 633 648 597Q646 592 598 404Q557 235 548 205Q515 105 433 42T263 -22Q171 -22 116 34T60 167V183Q60 201 115 421Q164 622 164 628Q164 635 107 637Z"></path><path id="MJX-1029-TEX-LO-2211" d="M60 948Q63 950 665 950H1267L1325 815Q1384 677 1388 669H1348L1341 683Q1320 724 1285 761Q1235 809 1174 838T1033 881T882 898T699 902H574H543H251L259 891Q722 258 724 252Q725 250 724 246Q721 243 460 -56L196 -356Q196 -357 407 -357Q459 -357 548 -357T676 -358Q812 -358 896 -353T1063 -332T1204 -283T1307 -196Q1328 -170 1348 -124H1388Q1388 -125 1381 -145T1356 -210T1325 -294L1267 -449L666 -450Q64 -450 61 -448Q55 -446 55 -439Q55 -437 57 -433L590 177Q590 178 557 222T452 366T322 544L56 909L55 924Q55 945 60 948Z"></path><path id="MJX-1029-TEX-I-1D465" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path id="MJX-1029-TEX-I-1D435" d="M231 637Q204 637 199 638T194 649Q194 676 205 682Q206 683 335 683Q594 683 608 681Q671 671 713 636T756 544Q756 480 698 429T565 360L555 357Q619 348 660 311T702 219Q702 146 630 78T453 1Q446 0 242 0Q42 0 39 2Q35 5 35 10Q35 17 37 24Q42 43 47 45Q51 46 62 46H68Q95 46 128 49Q142 52 147 61Q150 65 219 339T288 628Q288 635 231 637ZM649 544Q649 574 634 600T585 634Q578 636 493 637Q473 637 451 637T416 636H403Q388 635 384 626Q382 622 352 506Q352 503 351 500L320 374H401Q482 374 494 376Q554 386 601 434T649 544ZM595 229Q595 273 572 302T512 336Q506 337 429 337Q311 337 310 336Q310 334 293 263T258 122L240 52Q240 48 252 48T333 46Q422 46 429 47Q491 54 543 105T595 229Z"></path><path id="MJX-1029-TEX-N-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path id="MJX-1029-TEX-N-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path id="MJX-1029-TEX-N-30" d="M96 585Q152 666 249 666Q297 666 345 640T423 548Q460 465 460 320Q460 165 417 83Q397 41 362 16T301 -15T250 -22Q224 -22 198 -16T137 16T82 83Q39 165 39 320Q39 494 96 585ZM321 597Q291 629 250 629Q208 629 178 597Q153 571 145 525T137 333Q137 175 145 125T181 46Q209 16 250 16Q290 16 318 46Q347 76 354 130T362 333Q362 478 354 524T321 597Z"></path><path id="MJX-1029-TEX-N-2E" d="M78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mi"><use data-c="2203" xlink:href="#MJX-1029-TEX-N-2203"></use></g><g data-mml-node="mo" transform="translate(833.8,0)"><use data-c="3A" xlink:href="#MJX-1029-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(1389.6,0)"><use data-c="1D443" xlink:href="#MJX-1029-TEX-I-1D443"></use></g><g data-mml-node="mi" transform="translate(2140.6,0)"><use data-c="1D45F" xlink:href="#MJX-1029-TEX-I-1D45F"></use></g><g data-mml-node="mi" transform="translate(2591.6,0)"><use data-c="1D45C" xlink:href="#MJX-1029-TEX-I-1D45C"></use></g><g data-mml-node="mi" transform="translate(3076.6,0)"><use data-c="1D45D" xlink:href="#MJX-1029-TEX-I-1D45D"></use></g><g data-mml-node="msub" transform="translate(3857.3,0)"><g data-mml-node="mo"><use data-c="3D" xlink:href="#MJX-1029-TEX-N-3D"></use></g><g data-mml-node="TeXAtom" transform="translate(811,-150) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D451" xlink:href="#MJX-1029-TEX-I-1D451"></use></g><g data-mml-node="mi" transform="translate(520,0)"><use data-c="1D452" xlink:href="#MJX-1029-TEX-I-1D452"></use></g><g data-mml-node="mi" transform="translate(986,0)"><use data-c="1D453" xlink:href="#MJX-1029-TEX-I-1D453"></use></g></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(6082.2,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1029-TEX-N-7C"></use></g></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(6360.2,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1029-TEX-N-7C"></use></g></g><g data-mml-node="munder" transform="translate(6804.9,0)"><g data-mml-node="mo"><use data-c="220F" xlink:href="#MJX-1029-TEX-LO-220F"></use></g><g data-mml-node="TeXAtom" transform="translate(4.4,-1123.3) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D434" xlink:href="#MJX-1029-TEX-I-1D434"></use></g><g data-mml-node="mo" transform="translate(750,0)"><use data-c="3A" xlink:href="#MJX-1029-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(1028,0)"><use data-c="1D448" xlink:href="#MJX-1029-TEX-I-1D448"></use></g></g></g><g data-mml-node="munder" transform="translate(8249.6,0)"><g data-mml-node="mo"><use data-c="2211" xlink:href="#MJX-1029-TEX-LO-2211"></use></g><g data-mml-node="TeXAtom" transform="translate(156.3,-1123.3) scale(0.707)" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D465" xlink:href="#MJX-1029-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(572,0)"><use data-c="3A" xlink:href="#MJX-1029-TEX-N-3A"></use></g><g data-mml-node="mi" transform="translate(850,0)"><use data-c="1D434" xlink:href="#MJX-1029-TEX-I-1D434"></use></g></g></g><g data-mml-node="mi" transform="translate(9860.2,0)"><use data-c="1D435" xlink:href="#MJX-1029-TEX-I-1D435"></use></g><g data-mml-node="mo" transform="translate(10619.2,0)"><use data-c="28" xlink:href="#MJX-1029-TEX-N-28"></use></g><g data-mml-node="mi" transform="translate(11008.2,0)"><use data-c="1D465" xlink:href="#MJX-1029-TEX-I-1D465"></use></g><g data-mml-node="mo" transform="translate(11580.2,0)"><use data-c="29" xlink:href="#MJX-1029-TEX-N-29"></use></g><g data-mml-node="TeXAtom" data-mjx-texclass="ORD" transform="translate(11969.2,0)"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1029-TEX-N-7C"></use></g></g><g data-mml-node="msub" transform="translate(12247.2,0)"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mo" transform="translate(0 -0.5)"><use data-c="7C" xlink:href="#MJX-1029-TEX-N-7C"></use></g></g><g data-mml-node="mn" transform="translate(311,-150) scale(0.707)"><use data-c="30" xlink:href="#MJX-1029-TEX-N-30"></use></g></g><g data-mml-node="mo" transform="translate(12961.8,0)"><use data-c="2E" xlink:href="#MJX-1029-TEX-N-2E"></use></g></g></g></svg></mjx-container>
</p></section><section><h1>Bibliography</h1><br></section><section><h2>ANALYSIS</h2><p>[1]. L.Schwartz. Analyse Mathematique (1967)<br>
[2]. E.Bishop. <a href="https://archive.org/details/foundationsofcon0000bish">Foundations of Constructive Analysis</a> (1967)<br>
[3]. D.Bridges. <a href="https://core.ac.uk/download/pdf/82492373.pdf">Constructive mathematics: a foundation for computable analysis </a> (1999)<br>
[4]. W.Ziemer, M.Torres. <a href="https://www.math.purdue.edu/~torresm/pubs/Modern-real-analysis.pdf">Modern Real Analysis </a> (2017)<br>
[5]. A.Booij. <a href="https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf">Analysis in Univalent Type Theory</a> (2020)<br>
[6]. Z.Murray. <a href="https://arxiv.org/pdf/2205.08354">Constructive Real Numbers in the Agda</a> (2023)<br>
</p><p style="text-align:center;"><br>
<mjx-container class="MathJax" jax="SVG" display="true"><svg style="vertical-align: -1.948ex;" xmlns="http://www.w3.org/2000/svg" width="2.136ex" height="5.027ex" role="img" focusable="false" viewBox="0 -1361 944 2222" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1030-TEX-LO-222B" d="M114 -798Q132 -824 165 -824H167Q195 -824 223 -764T275 -600T320 -391T362 -164Q365 -143 367 -133Q439 292 523 655T645 1127Q651 1145 655 1157T672 1201T699 1257T733 1306T777 1346T828 1360Q884 1360 912 1325T944 1245Q944 1220 932 1205T909 1186T887 1183Q866 1183 849 1198T832 1239Q832 1287 885 1296L882 1300Q879 1303 874 1307T866 1313Q851 1323 833 1323Q819 1323 807 1311T775 1255T736 1139T689 936T633 628Q574 293 510 -5T410 -437T355 -629Q278 -862 165 -862Q125 -862 92 -831T55 -746Q55 -711 74 -698T112 -685Q133 -685 150 -700T167 -741Q167 -789 114 -798Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo" transform="translate(0 1)"><use data-c="222B" xlink:href="#MJX-1030-TEX-LO-222B"></use></g></g></g></svg></mjx-container>
<br><br>
</p><p>Присвячується Володимиру Олександровичу Клименку.
Механізована верифікація теорем функціонального аналізу
і теорії розподілів Лорана Шварца
у власній теорії типів на основі MLTT-72.
Повторна магістерська робота.
</p></section></div></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2021—2025 © <a rel="me" href="https://mathstodon.xyz/@5ht">Максим Сохацький</a></span></footer>