Logiweb dictionary of base

Up Help

0 0 base

1 2 [∗ ▷◁ ∗] 2 1 “ ∗ ”

3 0

4 2 ∗ , ∗ 5 3 ∗[ ∗]∗ 6 2 Preassociative ∗; ∗ 7 2 Postassociative ∗; ∗ 8 2 [∗], ∗ 9 1 priority ∗ end

10 1

∗ 11 0 ∗ 12 1 (∗)^{t} 13 2 string(∗) + ∗ 14 2 string(∗) ++ ∗

15 0 pyk

16 3 [∗ →^{∗} ∗]

17 2 ∗ linebreak[4] ∗

18 1 bracket ∗ end bracket
19 1 big bracket ∗ end bracket

20 1 $ ∗ $ 21 1 flush left [∗] 22 0 x 23 0 y 24 0 z

25 0 tex
26 0 name
27 0 prio

28 0 T 29 3 if(∗, ∗, ∗)

30 3 [∗ ⇒^{∗} ∗]

31 0 val

32 1 ∗ 33 1 !∗ 34 1 "∗ 35 1 #∗ 36 1 $∗ 37 1 %∗ 38 1 &∗ 39 1 ’∗ 40 1 (∗ 41 1 )∗ 42 1 ∗∗ 43 1 +∗ 44 1 , ∗ 45 1 -∗ 46 1 .∗ 47 1 /∗ 48 1 0∗ 49 1 1∗ 50 1 2∗ 51 1 3∗ 52 1 4∗ 53 1 5∗ 54 1 6∗ 55 1 7∗ 56 1 8∗ 57 1 9∗ 58 1 :∗ 59 1 ; ∗ 60 1 <∗ 61 1 =∗ 62 1 >∗

63 1 ?∗

64 1 @∗

65 1 A∗

66 1 B∗

67 1 C∗

68 1 D∗

69 1 E∗

70 1 F∗

71 1 G∗

72 1 H∗

73 1 I∗

74 1 J∗

75 1 K∗

76 1 L∗

77 1 M∗

78 1 N∗

79 1 O∗

80 1 P∗

81 1 Q∗

82 1 R∗

83 1 S∗

84 1 T∗

85 1 U∗

86 1 V∗

87 1 W∗

88 1 X∗

89 1 Y∗

90 1 Z∗

91 1 [∗

92 1 \∗

93 1 ]∗

94 1 ˆ ∗

95 1 ∗ 96 1 ‘∗

97 1 a∗

98 1 b∗

99 1 c∗

100 1 d∗

101 1 e∗

102 1 f∗

103 1 g∗

104 1 h∗

105 1 i∗

106 1 j∗

107 1 k∗

108 1 l∗

109 1 m∗

110 1 n∗

111 1 o∗

112 1 p∗

113 1 q∗

114 1 r∗

115 1 s∗

116 1 t∗

117 1 u∗

118 1 v∗

119 1 w∗

120 1 x∗

121 1 y∗

122 1 z∗

123 1 {∗

124 1 |∗

125 1 }∗

126 1 ˜ ∗

127 0 claim

128 0 ⊥

129 1 f(∗)

130 1 (∗)^{I} 131 0 F

132 0 \underline{0}
133 0 \underline{1}
134 0 \underline{2}
135 0 \underline{3}
136 0 \underline{4}
137 0 \underline{5}
138 0 \underline{6}
139 0 \underline{7}
140 0 \underline{8}
141 0 \underline{9}

142 0 0 143 0 1 144 0 2 145 0 3 146 0 4 147 0 5 148 0 6 149 0 7 150 0 8 151 0 9 152 0 a 153 0 b 154 0 c 155 0 d 156 0 e 157 0 f 158 0 g 159 0 h 160 0 i 161 0 j 162 0 k 163 0 l 164 0 m 165 0 n 166 0 o 167 0 p 168 0 q 169 0 r 170 0 s 171 0 t 172 0 u 173 0 v 174 0 w 175 1 (∗)^{M} 176 3 If(∗, ∗, ∗) 177 2 array{∗} ∗ end array 178 0 l 179 0 c 180 0 r

181 0 empty

182 3 ⟨∗ | ∗:= ∗⟩ 183 1 M(∗) 184 1 Ũ(∗) 185 1 U(∗) 186 1 U^{M}(∗) 187 2 apply(∗, ∗) 188 2 apply_{1}(∗, ∗) 189 1 identifier(∗) 190 2 identifier_{1}(∗, ∗) 191 2 array-plus(∗, ∗) 192 3 array-remove(∗, ∗, ∗) 193 4 array-put(∗, ∗, ∗, ∗) 194 5 array-add(∗, ∗, ∗, ∗, ∗) 195 2 bit(∗, ∗) 196 2 bit_{1}(∗, ∗) 197 0 rack

198 0 "vector"
199 0 "bibliography"
200 0 "dictionary"
201 0 "body"
202 0 "codex"
203 0 "expansion"
204 0 "code"
205 0 "cache"
206 0 "diagnose"
207 0 "pyk"
208 0 "tex"
209 0 "texname"
210 0 "value"
211 0 "message"
212 0 "macro"
213 0 "definition"
214 0 "unpack"
215 0 "claim"
216 0 "priority"
217 0 "lambda"
218 0 "apply"
219 0 "true"
220 0 "if"
221 0 "quote"
222 0 "proclaim"
223 0 "define"
224 0 "introduce"
225 0 "hide"
226 0 "pre"
227 0 "post"

228 3 E(∗, ∗, ∗)

229 5 E_{2}(∗, ∗, ∗, ∗, ∗)

230 4 E_{3}(∗, ∗, ∗, ∗)

231 4 E_{4}(∗, ∗, ∗, ∗)

232 3 lookup(∗, ∗, ∗) 233 4 abstract(∗, ∗, ∗, ∗) 234 1 ⌈∗⌉ 235 3 M(∗, ∗, ∗) 236 4 M_{2}(∗, ∗, ∗, ∗) 237 3 M^{∗}(∗, ∗, ∗)

238 0 macro

239 0 s_{0} 240 2 zip(∗, ∗) 241 3 assoc_{1}(∗, ∗, ∗) 242 1 (∗)^{p}

243 0 self

244 2 [∗ ¨= ∗] 245 2 [∗ ˙= ∗] 246 2 [∗ ´= ∗]

247 2 [∗ =^{pyk} ∗]

248 2 [∗ =^{tex} ∗]

249 2 [∗ =^{name} ∗]

250 1 Priority table[∗]

251 0 M̃_{1}

252 1 M̃_{2}(∗) 253 1 M̃_{3}(∗) 254 4 M̃_{4}(∗, ∗, ∗, ∗) 255 3 M̃(∗, ∗, ∗) 256 3 Q̃(∗, ∗, ∗) 257 3 Q̃_{2}(∗, ∗, ∗) 258 4 Q̃_{3}(∗, ∗, ∗, ∗) 259 3 Q̃^{∗}(∗, ∗, ∗) 260 1 (∗)

261 1 (∗)

262 1 display(∗) 263 1 statement(∗) 264 1 [∗]^{·} 265 1 [∗]^{−} 266 2 aspect(∗, ∗) 267 3 aspect(∗, ∗, ∗) 268 1 ⟨∗⟩ 269 1 tuple_{1}(∗) 270 1 tuple_{2}(∗) 271 2 let_{2}(∗, ∗) 272 2 let_{1}(∗, ∗)

273 2 [∗ =^{claim} ∗]

274 0 checker

275 2 check(∗, ∗) 276 3 check_{2}(∗, ∗, ∗) 277 3 check_{3}(∗, ∗, ∗) 278 2 check^{∗}(∗, ∗) 279 3 check_{2}^{∗}(∗, ∗, ∗) 280 1 [∗]^{·} 281 1 [∗]^{−} 282 1 [∗]^{∘} 283 0 msg

284 2 [∗ =^{msg} ∗]

285 0 <stmt> 286 0 stmt

287 2 [∗ =^{stmt} ∗]

288 0 HeadNil′ 289 0 HeadPair′ 290 0 Transitivity′

291 0 ⊥ ⊥

292 0 Contra′ 293 0 T′_{E} 294 0 L_{1}

295 1 \underline{∗}

296 0 A 297 0 B 298 0 C 299 0 D 300 0 E 301 0 F 302 0 G 303 0 H 304 0 I 305 0 J 306 0 K 307 0 L 308 0 M 309 0 N 310 0 O 311 0 P 312 0 Q 313 0 R 314 0 S 315 0 T 316 0 U 317 0 V 318 0 W 319 0 X 320 0 Y 321 0 Z 322 3 ⟨∗ | ∗:= ∗⟩ 323 3 ⟨^{∗}∗ | ∗:= ∗⟩ 324 0 ∅ 325 0 Remainder 326 1 (∗)^{v} 327 4 intro(∗, ∗, ∗, ∗) 328 3 intro(∗, ∗, ∗) 329 2 error(∗, ∗) 330 2 error_{2}(∗, ∗) 331 3 proof(∗, ∗, ∗)

332 2 proof_{2}(∗, ∗) 333 2 S(∗, ∗) 334 2 S^{I}(∗, ∗) 335 2 S^{⊳} (∗, ∗) 336 3 S_{1}^{⊳} (∗, ∗, ∗) 337 2 S^{E}(∗, ∗) 338 3 S_{1}^{E}(∗, ∗, ∗) 339 2 S^{+}(∗, ∗) 340 3 S_{1}^{+}(∗, ∗, ∗) 341 2 S^{−}(∗, ∗) 342 3 S_{1}^{−}(∗, ∗, ∗) 343 2 S^{∗}(∗, ∗) 344 3 S_{1}^{∗}(∗, ∗, ∗) 345 4 S_{2}^{∗}(∗, ∗, ∗, ∗) 346 2 S^{@}(∗, ∗) 347 3 S_{1}^{@}(∗, ∗, ∗) 348 2 S^{⊢}(∗, ∗) 349 4 S_{1}^{⊢}(∗, ∗, ∗, ∗) 350 2 S⊢ ⊢(∗, ∗)

351 4 S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)

352 2 S^{i.e.}(∗, ∗) 353 4 S_{1}^{i.e.}(∗, ∗, ∗, ∗) 354 5 S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗) 355 2 S^{∀}(∗, ∗) 356 4 S_{1}^{∀}(∗, ∗, ∗, ∗) 357 2 S^{;}(∗, ∗) 358 3 S_{1}^{;}(∗, ∗, ∗) 359 4 S_{2}^{;}(∗, ∗, ∗, ∗) 360 1 T (∗) 361 3 claims(∗, ∗, ∗) 362 3 claims_{2}(∗, ∗, ∗) 363 0 <proof> 364 0 proof 365 2 [Lemma ∗: ∗] 366 2 [Proof of ∗: ∗] 367 3 [∗ lemma ∗: ∗] 368 3 [∗ antilemma ∗: ∗] 369 3 [∗ rule ∗: ∗] 370 3 [∗ antirule ∗: ∗]

371 0 verifier

372 1 V_{1}(∗) 373 2 V_{2}(∗, ∗) 374 4 V_{3}(∗, ∗, ∗, ∗) 375 2 V_{4}(∗, ∗) 376 4 V_{5}(∗, ∗, ∗, ∗) 377 4 V_{6}(∗, ∗, ∗, ∗) 378 4 V_{7}(∗, ∗, ∗, ∗) 379 2 Cut(∗, ∗) 380 1 Head_{⊕}(∗) 381 1 Tail_{⊕}(∗) 382 2 rule_{1}(∗, ∗) 383 2 rule(∗, ∗) 384 0 Rule tactic 385 2 Plus(∗, ∗) 386 1 [Theory ∗] 387 2 theory_{2}(∗, ∗) 388 2 theory_{3}(∗, ∗) 389 3 theory_{4}(∗, ∗, ∗) 390 0 HeadNil′′ 391 0 HeadPair′′ 392 0 Transitivity′′ 393 0 Contra′′ 394 0 HeadNil 395 0 HeadPair 396 0 Transitivity 397 0 Contra 398 0 T_{E} 399 0 ragged right 400 0 ragged right expansion 401 3 parm(∗, ∗, ∗) 402 3 parm^{∗}(∗, ∗, ∗) 403 2 inst(∗, ∗) 404 2 inst^{∗}(∗, ∗) 405 3 occur(∗, ∗, ∗) 406 3 occur^{∗}(∗, ∗, ∗) 407 3 unify(∗ = ∗, ∗) 408 3 unify^{∗}(∗ = ∗, ∗) 409 3 unify_{2}(∗ = ∗, ∗) 410 0 L_{a} 411 0 L_{b} 412 0 L_{c} 413 0 L_{d} 414 0 L_{e} 415 0 L_{f} 416 0 L_{g} 417 0 L_{h} 418 0 L_{i} 419 0 L_{j} 420 0 L_{k} 421 0 L_{l} 422 0 L_{m} 423 0 L_{n} 424 0 L_{o} 425 0 L_{p} 426 0 L_{q} 427 0 L_{r} 428 0 L_{s} 429 0 L_{t} 430 0 L_{u} 431 0 L_{v} 432 0 L_{w} 433 0 L_{x} 434 0 L_{y} 435 0 L_{z} 436 0 L_{A} 437 0 L_{B} 438 0 L_{C} 439 0 L_{D} 440 0 L_{E} 441 0 L_{F} 442 0 L_{G} 443 0 L_{H} 444 0 L_{I} 445 0 L_{J} 446 0 L_{K} 447 0 L_{L} 448 0 L_{M} 449 0 L_{N} 450 0 L_{O} 451 0 L_{P} 452 0 L_{Q} 453 0 L_{R} 454 0 L_{S} 455 0 L_{T} 456 0 L_{U} 457 0 L_{V} 458 0 L_{W} 459 0 L_{X} 460 0 L_{Y} 461 0 L_{Z} 462 0 L_{?} 463 0 Reflexivity 464 0 Reflexivity_{1} 465 0 Commutativity 466 0 Commutativity_{1} 467 0 <tactic> 468 0 tactic

469 2 [∗ =^{tactic} ∗]

470 3 P(∗, ∗, ∗) 471 3 P^{∗}(∗, ∗, ∗) 472 0 p_{0} 473 2 conclude_{1}(∗, ∗) 474 3 conclude_{2}(∗, ∗, ∗) 475 4 conclude_{3}(∗, ∗, ∗, ∗) 476 2 conclude_{4}(∗, ∗) 477 2 ∗ {∗} 478 5 ∗/indexintro(∗, ∗, ∗, ∗) 479 4 ∗/intro(∗, ∗, ∗) 480 6 ∗/bothintro(∗, ∗, ∗, ∗, ∗) 481 5 ∗/nameintro(∗, ∗, ∗, ∗) 482 1 ∗′ 483 2 ∗[ ∗] 484 3 ∗[∗→∗] 485 3 ∗[∗⇒∗] 486 1 ∗0 487 1 ∗1 488 0 0b 489 2 ∗-color(∗) 490 2 ∗-color^{∗}(∗) 491 1 ∗^{H} 492 1 ∗^{T} 493 1 ∗^{U} 494 1 ∗^{h} 495 1 ∗^{t} 496 1 ∗^{s} 497 1 ∗^{c} 498 1 ∗^{d} 499 1 ∗^{a} 500 1 ∗^{C} 501 1 ∗^{M} 502 1 ∗^{B} 503 1 ∗^{r} 504 1 ∗^{i} 505 1 ∗^{d} 506 1 ∗^{R} 507 1 ∗^{0} 508 1 ∗^{1} 509 1 ∗^{2} 510 1 ∗^{3} 511 1 ∗^{4} 512 1 ∗^{5} 513 1 ∗^{6} 514 1 ∗^{7} 515 1 ∗^{8} 516 1 ∗^{9} 517 1 ∗^{E} 518 1 ∗^{V} 519 1 ∗^{C} 520 1 ∗^{C^{∗}} 521 1 newline ∗ 522 1 macro newline ∗ 523 2 ∗ ’ ∗ 524 2 ∗ ‘ ∗ 525 2 ∗ · ∗ 526 2 ∗ ·_{0} ∗ 527 2 ∗ + ∗ 528 2 ∗ +_{0} ∗ 529 2 ∗ +_{1} ∗ 530 2 ∗ − ∗ 531 2 ∗ −_{0} ∗ 532 2 ∗ −_{1} ∗ 533 2 ∗ ∪ {∗} 534 2 ∗ ∪ ∗ 535 2 ∗\{∗} 536 2 ∗ ˙. . ∗ 537 2 ∗ \underline{˙. .} ∗ 538 2 ∗ \underline{: :} ∗ 539 2 ∗ \underline{+2∗} ∗ 540 2 ∗ : : ∗ 541 2 ∗ +2∗ ∗ 542 2 ∗, ∗

543 2 ∗ ≈^{B} ∗

544 2 ∗ ≈^{D} ∗

545 2 ∗ ≈^{C} ∗

546 2 ∗ ≈^{P} ∗

547 2 ∗ ≈ ∗ 548 2 ∗ = ∗

549 2 ∗ →^{+} ∗

550 2 ∗ =^{t} ∗

551 2 ∗ =^{t^{∗}} ∗

552 2 ∗ =^{r} ∗

553 2 ∗ ∈_{t} ∗ 554 2 ∗ ⊆_{T} ∗

555 2 ∗ =^{T} ∗

556 2 ∗ =^{s} ∗

557 2 ∗ free in ∗ 558 2 ∗ free in^{∗} ∗ 559 3 ∗ free for ∗ in ∗ 560 3 ∗ free for^{∗} ∗ in ∗ 561 2 ∗ ∈_{c} ∗ 562 2 ∗ < ∗ 563 2 ∗ <′ ∗ 564 2 ∗ ≤′ ∗ 565 1 ¬∗ 566 2 ∗ ∧ ∗ 567 2 ∗ ¨∧ ∗ 568 2 ∗ ˜∧ ∗ 569 2 ∗ ∧_{c} ∗ 570 2 ∗ ∨ ∗ 571 2 ∗ ∥ ∗ 572 2 ∗ ¨∨ ∗ 573 2 ∗ ¨⇒ ∗ 574 2 ∗ : ∗ 575 2 ∗ spy ∗ 576 2 ∗!∗

577 3 ∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix}

578 2 λ ∗ .∗ 579 2 Λ ∗ .∗ 580 1 Λ∗ 581 3 if ∗ then ∗ else ∗ 582 3 let ∗ = ∗ in ∗ 583 3 let ∗ ¨= ∗ in ∗ 584 1 ∗^{I} 585 1 ∗^{⊳} 586 1 ∗^{V} 587 1 ∗^{+} 588 1 ∗^{−} 589 1 ∗^{∗} 590 2 ∗ @ ∗ 591 2 ∗ ⊳ ∗ 592 2 ∗ ⊳ ⊳ ∗ 593 2 ∗ ≫ ∗ 594 2 ∗ ⊢ ∗ 595 2 ∗ ⊢⊢ ∗ 596 2 ∗ i.e. ∗ 597 2 ∀∗: ∗ 598 2 ∗ ⊕ ∗ 599 2 ∗; ∗ 600 2 ∗ proves ∗ 601 3 ∗ proof of ∗ : ∗ 602 4 Line ∗ : ∗ ≫ ∗; ∗ 603 2 Last line ∗ ≫ ∗ □ 604 3 Line ∗ : Premise ≫ ∗; ∗ 605 3 Line ∗ : Side-condition ≫ ∗; ∗ 606 2 Arbitrary ≫ ∗; ∗ 607 3 Local ≫ ∗ = ∗; ∗ 608 2 ∗&∗ 609 2 ∗\\∗

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-06.UTC:07:18:19.012409 = MJD-53892.TAI:07:18:52.012409 = LGT-4656295132012409e-6