Logiweb dictionary of base

Up Help

0 0 base

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

3 0

4 2 ∗ then ∗ 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 1 bracket ∗ end bracket
16 1 big bracket ∗ end bracket
17 1 math ∗ end math

18 1 flush left [∗] 19 0 x 20 0 y 21 0 z

22 3 [∗ →^{∗} ∗]

23 0 pyk
24 0 tex
25 0 name
26 0 prio

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

29 3 [∗ ⇒^{∗} ∗]

30 0 val
31 0 claim

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 ⊥

128 1 f(∗)

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

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

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

180 0 empty

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

197 0 "vector"

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

227 3 E(∗, ∗, ∗)

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

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

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

231 3 lookup(∗, ∗, ∗)

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

237 0 macro

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

242 0 self

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

246 2 [∗ =^{pyk} ∗]

247 2 [∗ =^{tex} ∗]

248 2 [∗ =^{name} ∗]

249 1 Priority table[∗]

250 0 M̃_{1}

251 1 M̃_{2}(∗) 252 1 M̃_{3}(∗) 253 4 M̃_{4}(∗, ∗, ∗, ∗) 254 3 M̃(∗, ∗, ∗) 255 3 Q̃(∗, ∗, ∗) 256 3 Q̃_{2}(∗, ∗, ∗) 257 4 Q̃_{3}(∗, ∗, ∗, ∗) 258 3 Q̃^{∗}(∗, ∗, ∗) 259 1 (∗) 260 2 aspect(∗, ∗) 261 3 aspect(∗, ∗, ∗) 262 1 ⟨∗⟩ 263 1 tuple_{1}(∗) 264 1 tuple_{2}(∗)

265 2 let_{2}(∗, ∗) 266 2 let_{1}(∗, ∗)

267 2 [∗ =^{claim} ∗]

268 0 checker

269 2 check(∗, ∗) 270 3 check_{2}(∗, ∗, ∗) 271 3 check_{3}(∗, ∗, ∗) 272 2 check^{∗}(∗, ∗) 273 3 check_{2}^{∗}(∗, ∗, ∗) 274 1 [∗]^{·} 275 1 [∗]^{−} 276 1 [∗]^{∘} 277 0 msg

278 2 [∗ =^{msg} ∗]

279 0 <stmt> 280 0 stmt

281 2 [∗ =^{stmt} ∗]

282 0 HeadNil′ 283 0 HeadPair′ 284 0 Transitivity′

285 0 ⊥ ⊥

286 0 Contra′ 287 0 T′_{E} 288 0 L_{1}

289 1 \underline{∗}

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

332 3 S_{1}^{E}(∗, ∗, ∗) 333 2 S^{+}(∗, ∗) 334 3 S_{1}^{+}(∗, ∗, ∗) 335 2 S^{−}(∗, ∗) 336 3 S_{1}^{−}(∗, ∗, ∗) 337 2 S^{∗}(∗, ∗) 338 3 S_{1}^{∗}(∗, ∗, ∗) 339 4 S_{2}^{∗}(∗, ∗, ∗, ∗) 340 2 S^{@}(∗, ∗) 341 3 S_{1}^{@}(∗, ∗, ∗) 342 2 S^{⊢}(∗, ∗) 343 4 S_{1}^{⊢}(∗, ∗, ∗, ∗) 344 2 S⊢ ⊢(∗, ∗)

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

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

365 0 verifier

366 1 V_{1}(∗) 367 2 V_{2}(∗, ∗) 368 4 V_{3}(∗, ∗, ∗, ∗) 369 2 V_{4}(∗, ∗) 370 4 V_{5}(∗, ∗, ∗, ∗) 371 4 V_{6}(∗, ∗, ∗, ∗) 372 4 V_{7}(∗, ∗, ∗, ∗) 373 2 Cut(∗, ∗) 374 1 Head_{⊕}(∗) 375 1 Tail_{⊕}(∗) 376 2 rule_{1}(∗, ∗) 377 2 rule(∗, ∗) 378 0 Rule tactic 379 2 Plus(∗, ∗) 380 1 [Theory ∗] 381 2 theory_{2}(∗, ∗) 382 2 theory_{3}(∗, ∗) 383 3 theory_{4}(∗, ∗, ∗) 384 0 HeadNil′′ 385 0 HeadPair′′ 386 0 Transitivity′′ 387 0 Contra′′ 388 0 HeadNil 389 0 HeadPair 390 0 Transitivity 391 0 Contra 392 0 T_{E} 393 0 ragged right 394 0 ragged right expansion 395 3 parm(∗, ∗, ∗) 396 3 parm^{∗}(∗, ∗, ∗) 397 2 inst(∗, ∗) 398 2 inst^{∗}(∗, ∗) 399 3 occur(∗, ∗, ∗)

400 3 occur^{∗}(∗, ∗, ∗) 401 3 unify(∗ = ∗, ∗) 402 3 unify^{∗}(∗ = ∗, ∗) 403 3 unify_{2}(∗ = ∗, ∗) 404 0 L_{a} 405 0 L_{b} 406 0 L_{c} 407 0 L_{d} 408 0 L_{e} 409 0 L_{f} 410 0 L_{g} 411 0 L_{h} 412 0 L_{i} 413 0 L_{j} 414 0 L_{k} 415 0 L_{l} 416 0 L_{m} 417 0 L_{n} 418 0 L_{o} 419 0 L_{p} 420 0 L_{q} 421 0 L_{r} 422 0 L_{s} 423 0 L_{t} 424 0 L_{u} 425 0 L_{v} 426 0 L_{w} 427 0 L_{x} 428 0 L_{y} 429 0 L_{z} 430 0 L_{A} 431 0 L_{B} 432 0 L_{C} 433 0 L_{D} 434 0 L_{E} 435 0 L_{F} 436 0 L_{G} 437 0 L_{H} 438 0 L_{I} 439 0 L_{J} 440 0 L_{K} 441 0 L_{L} 442 0 L_{M} 443 0 L_{N} 444 0 L_{O} 445 0 L_{P} 446 0 L_{Q} 447 0 L_{R} 448 0 L_{S} 449 0 L_{T} 450 0 L_{U} 451 0 L_{V} 452 0 L_{W} 453 0 L_{X} 454 0 L_{Y} 455 0 L_{Z} 456 0 L_{?} 457 0 Reflexivity 458 0 Reflexivity_{1} 459 0 Commutativity 460 0 Commutativity_{1} 461 0 <tactic> 462 0 tactic

463 2 [∗ =^{tactic} ∗]

464 3 P(∗, ∗, ∗) 465 3 P^{∗}(∗, ∗, ∗) 466 0 p_{0} 467 2 conclude_{1}(∗, ∗)

468 3 conclude_{2}(∗, ∗, ∗) 469 4 conclude_{3}(∗, ∗, ∗, ∗) 470 2 ∗ {∗} 471 1 ∗′ 472 2 ∗[ ∗] 473 3 ∗[∗→∗] 474 3 ∗[∗⇒∗] 475 1 newline ∗ 476 1 macro newline ∗ 477 1 ∗0 478 1 ∗1 479 0 0b 480 2 ∗-color(∗) 481 2 ∗-color^{∗}(∗) 482 2 ∗ ’ ∗ 483 2 ∗ ‘ ∗ 484 1 ∗^{H} 485 1 ∗^{T} 486 1 ∗^{U} 487 1 ∗^{h} 488 1 ∗^{t} 489 1 ∗^{s} 490 1 ∗^{c} 491 1 ∗^{d} 492 1 ∗^{a} 493 1 ∗^{C} 494 1 ∗^{M} 495 1 ∗^{B} 496 1 ∗^{r} 497 1 ∗^{i} 498 1 ∗^{d} 499 1 ∗^{R} 500 1 ∗^{0} 501 1 ∗^{1} 502 1 ∗^{2}

503 1 ∗^{3}

504 1 ∗^{4}

505 1 ∗^{5}

506 1 ∗^{6}

507 1 ∗^{7}

508 1 ∗^{8}

509 1 ∗^{9}

510 1 ∗^{E}

511 1 ∗^{V}

512 1 ∗^{C}

513 1 ∗^{C^{∗}}

514 2 ∗ · ∗

515 2 ∗ ·_{0} ∗

516 2 ∗ + ∗

517 2 ∗ +_{0} ∗

518 2 ∗ +_{1} ∗

519 2 ∗ − ∗

520 2 ∗ −_{0} ∗

521 2 ∗ −_{1} ∗

522 2 ∗ ∪ {∗}

523 2 ∗ ∪ ∗

524 2 ∗\{∗}

525 2 ∗ ˙. . ∗

526 2 ∗ \underline{˙. .} ∗

527 2 ∗ \underline{: :} ∗

528 2 ∗ \underline{+2∗} ∗

529 2 ∗ : : ∗

530 2 ∗ +2∗ ∗

531 2 ∗, ∗

532 2 ∗ ≈^{B} ∗

533 2 ∗ ≈^{D} ∗

534 2 ∗ ≈^{C} ∗

535 2 ∗ ≈^{P} ∗

536 2 ∗ ≈ ∗ 537 2 ∗ = ∗

538 2 ∗ →^{+} ∗

539 2 ∗ =^{t} ∗

540 2 ∗ =^{t^{∗}} ∗

541 2 ∗ =^{r} ∗

542 2 ∗ ∈_{t} ∗ 543 2 ∗ ⊆_{T} ∗

544 2 ∗ =^{T} ∗

545 2 ∗ =^{s} ∗

546 2 ∗ free in ∗ 547 2 ∗ free in^{∗} ∗ 548 3 ∗ free for ∗ in ∗ 549 3 ∗ free for^{∗} ∗ in ∗ 550 2 ∗ ∈_{c} ∗ 551 2 ∗ < ∗ 552 2 ∗ <′ ∗ 553 2 ∗ ≤′ ∗ 554 1 ¬∗ 555 2 ∗ ∧ ∗ 556 2 ∗ ¨∧ ∗ 557 2 ∗ ˜∧ ∗ 558 2 ∗ ∧_{c} ∗ 559 2 ∗ ∨ ∗ 560 2 ∗ ∥ ∗ 561 2 ∗ ¨∨ ∗ 562 2 ∗ ¨⇒ ∗ 563 2 ∗ : ∗ 564 2 ∗!∗

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

566 2 λ ∗ .∗ 567 1 Λ∗ 568 3 if ∗ then ∗ else ∗ 569 3 let ∗ = ∗ in ∗ 570 3 let ∗ ¨= ∗ in ∗ 571 1 ∗^{I} 572 1 ∗^{⊳} 573 1 ∗^{V} 574 1 ∗^{+} 575 1 ∗^{−} 576 1 ∗^{∗} 577 2 ∗ @ ∗ 578 2 ∗ ⊳ ∗ 579 2 ∗ ⊳ ⊳ ∗ 580 2 ∗ ≫ ∗ 581 2 ∗ ⊢ ∗ 582 2 ∗ ⊢⊢ ∗ 583 2 ∗ i.e. ∗ 584 2 ∀∗: ∗ 585 2 ∗ ⊕ ∗ 586 2 ∗; ∗ 587 2 ∗ proves ∗ 588 3 ∗ proof of ∗ : ∗ 589 4 Line ∗ : ∗ ≫ ∗; ∗ 590 2 Last line ∗ ≫ ∗ □ 591 3 Line ∗ : Premise ≫ ∗; ∗ 592 3 Line ∗ : Side-condition ≫ ∗; ∗ 593 2 Arbitrary ≫ ∗; ∗ 594 3 Local ≫ ∗ = ∗; ∗ 595 2 ∗&∗ 596 2 ∗\\∗

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-06-03.UTC:15:49:33.495567 = MJD-53524.TAI:15:50:05.495567 = LGT-4624530605495567e-6