Logiweb dictionary of ijcar base

Up Help

0 0 ijcar 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 $ ∗ $ 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 1 (∗)

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

272 2 [∗ =^{claim} ∗]

273 0 checker

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

283 2 [∗ =^{msg} ∗]

284 0 <stmt> 285 0 stmt

286 2 [∗ =^{stmt} ∗]

287 0 HeadNil′ 288 0 HeadPair′ 289 0 Transitivity′

290 0 ⊥ ⊥

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

294 1 \underline{∗}

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

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

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

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

370 0 verifier

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

468 2 [∗ =^{tactic} ∗]

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

542 2 ∗ ≈^{B} ∗

543 2 ∗ ≈^{D} ∗

544 2 ∗ ≈^{C} ∗

545 2 ∗ ≈^{P} ∗

546 2 ∗ ≈ ∗ 547 2 ∗ = ∗

548 2 ∗ →^{+} ∗

549 2 ∗ =^{t} ∗

550 2 ∗ =^{t^{∗}} ∗

551 2 ∗ =^{r} ∗

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

554 2 ∗ =^{T} ∗

555 2 ∗ =^{s} ∗

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

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

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

The pyk compiler, version 0.grue.20060417 by Klaus Grue GRD-2006-02-24.UTC:10:23:46.350024 = MJD-53790.TAI:10:24:19.350024 = LGT-4647493459350024e-6