QLE Home Quantum Logic Explorer This is the GIF version.
Change to Unicode version

List of Theorems
RefDescription
id 59 Identity law.
tt 60 Justification of definitio...
cm 61 Commutative inference rule...
tr 62 Transitive inference rule ...
3tr1 63 Transitive inference usefu...
3tr2 64 Transitive inference usefu...
3tr 65 Triple transitive inference.
con1 66 Contraposition inference.
con2 67 Contraposition inference.
con3 68 Contraposition inference.
con4 69 Contraposition inference.
lor 70 Inference introducing disj...
ror 71 Inference introducing disj...
2or 72 Join both sides with disju...
orcom 73 Commutative law.
ancom 74 Commutative law.
orass 75 Associative law.
anass 76 Associative law.
lan 77 Introduce conjunct on left.
ran 78 Introduce conjunct on right.
2an 79 Conjoin both sides of hypo...
or12 80 Swap disjuncts.
an12 81 Swap conjuncts.
or32 82 Swap disjuncts.
an32 83 Swap conjuncts.
or4 84 Swap disjuncts.
or42 85 Rearrange disjuncts.
an4 86 Swap conjuncts.
oran 87 Disjunction expressed with...
anor1 88 Conjunction expressed with...
anor2 89 Conjunction expressed with...
anor3 90 Conjunction expressed with...
oran1 91 Disjunction expressed with...
oran2 92 Disjunction expressed with...
oran3 93 Disjunction expressed with...
dfb 94 Biconditional expressed wi...
dfnb 95 Negated biconditional.
bicom 96 Commutative law.
lbi 97 Introduce biconditional to...
rbi 98 Introduce biconditional to...
2bi 99 Join both sides with bicon...
dff2 100 Alternate defintion of "fa...
dff 101 Alternate defintion of "fa...
or0 102 Disjunction with 0.
or0r 103 Disjunction with 0.
or1 104 Disjunction with 1.
or1r 105 Disjunction with 1.
an1 106 Conjunction with 1.
an1r 107 Conjunction with 1.
an0 108 Conjunction with 0.
an0r 109 Conjunction with 0.
oridm 110 Idempotent law.
anidm 111 Idempotent law.
orordi 112 Distribution of disjunctio...
orordir 113 Distribution of disjunctio...
anandi 114 Distribution of conjunctio...
anandir 115 Distribution of conjunctio...
biid 116 Identity law.
1b 117 Identity law.
bi1 118 Identity inference.
1bi 119 Identity inference.
orabs 120 Absorption law.
anabs 121 Absorption law.
conb 122 Contraposition law.
leoa 123 Relation between two metho...
leao 124 Relation between two metho...
mi 125 Mittelstaedt implication.
di 126 Dishkant implication.
omlem1 127 Lemma in proof of Th. 1 of...
omlem2 128 Lemma in proof of Th. 1 of...
df2le1 135 Alternate definition of 'l...
df2le2 136 Alternate definition of 'l...
letr 137 Transitive law for l.e.
bltr 138 Transitive inference.
lbtr 139 Transitive inference.
le3tr1 140 Transitive inference usefu...
le3tr2 141 Transitive inference usefu...
bile 142 Biconditional to l.e.
qlhoml1a 143 An ortholattice inequality...
qlhoml1b 144 An ortholattice inequality...
lebi 145 L.e. to biconditional.
le1 146 Anything is l.e. 1.
le0 147 0 is l.e. anything.
leid 148 Identity law for less-than...
ler 149 Add disjunct to right of l.e.
lerr 150 Add disjunct to right of l.e.
lel 151 Add conjunct to left of l.e.
leror 152 Add disjunct to right of b...
leran 153 Add conjunct to right of b...
lecon 154 Contrapositive for l.e.
lecon1 155 Contrapositive for l.e.
lecon2 156 Contrapositive for l.e.
lecon3 157 Contrapositive for l.e.
leo 158 L.e. absorption.
leor 159 L.e. absorption.
lea 160 L.e. absorption.
lear 161 L.e. absorption.
leao1 162 L.e. absorption.
leao2 163 L.e. absorption.
leao3 164 L.e. absorption.
leao4 165 L.e. absorption.
lelor 166 Add disjunct to left of bo...
lelan 167 Add conjunct to left of bo...
le2or 168 Disjunction of 2 l.e.'s.
le2an 169 Conjunction of 2 l.e.'s.
lel2or 170 Disjunction of 2 l.e.'s.
lel2an 171 Conjunction of 2 l.e.'s.
ler2or 172 Disjunction of 2 l.e.'s.
ler2an 173 Conjunction of 2 l.e.'s.
ledi 174 Half of distributive law.
ledir 175 Half of distributive law.
ledio 176 Half of distributive law.
ledior 177 Half of distributive law.
comm0 178 Commutation with 0. Kalmb...
comm1 179 Commutation with 1. Kalmb...
lecom 180 Comparable elements commut...
bctr 181 Transitive inference.
cbtr 182 Transitive inference.
comcom2 183 Commutation equivalence. ...
comorr 184 Commutation law. Does not...
coman1 185 Commutation law. Does not...
coman2 186 Commutation law. Does not...
comid 187 Identity law for commutati...
distlem 188 Distributive law inference...
str 189 Strengthening rule.
cmtrcom 190 Commutative law for commut...
wa1 191 Weak A1.
wa2 192 Weak A2.
wa3 193 Weak A3.
wa4 194 Weak A4.
wa5 195 Weak A5.
wa6 196 Weak A6.
wr1 197 Weak R1.
wr3 198 Weak R3.
wr4 199 Weak R4.
wa5b 200 Absorption law.
wa5c 201 Absorption law.
wcon 202 Contraposition law.
wancom 203 Commutative law.
wanass 204 Associative law.
wwbmp 205 Weak weak equivalential de...
wwbmpr 206 Weak weak equivalential de...
wcon1 207 Weak contraposition.
wcon2 208 Weak contraposition.
wcon3 209 Weak contraposition.
wlem3.1 210 Weak analogue to lemma use...
woml 211 Theorem structurally simil...
wwoml2 212 Weak orthomodular law.
wwoml3 213 Weak orthomodular law.
wwcomd 214 Commutation dual (weak). ...
wwcom3ii 215 Lemma 3(ii) (weak) of Kalm...
wwfh1 216 Foulis-Holland Theorem (we...
wwfh2 217 Foulis-Holland Theorem (we...
wwfh3 218 Foulis-Holland Theorem (we...
wwfh4 219 Foulis-Holland Theorem (we...
womao 220 Weak OM-like absorption la...
womaon 221 Weak OM-like absorption la...
womaa 222 Weak OM-like absorption la...
womaan 223 Weak OM-like absorption la...
anorabs2 224 Absorption law for orthola...
anorabs 225 Absorption law for orthola...
ska2a 226 Axiom KA2a in Pavicic and ...
ska2b 227 Axiom KA2b in Pavicic and ...
ka4lemo 228 Lemma for KA4 soundness (O...
ka4lem 229 Lemma for KA4 soundness (A...
sklem 230 Soundness lemma.
ska1 231 Soundness theorem for Kalm...
ska3 232 Soundness theorem for Kalm...
ska5 233 Soundness theorem for Kalm...
ska6 234 Soundness theorem for Kalm...
ska7 235 Soundness theorem for Kalm...
ska8 236 Soundness theorem for Kalm...
ska9 237 Soundness theorem for Kalm...
ska10 238 Soundness theorem for Kalm...
ska11 239 Soundness theorem for Kalm...
ska12 240 Soundness theorem for Kalm...
ska13 241 Soundness theorem for Kalm...
skr0 242 Soundness theorem for Kalm...
wlem1 243 Lemma for 2-variable WOML ...
ska15 244 Soundness theorem for Kalm...
skmp3 245 Soundness proof for KMP3.
lei3 246 L.e. to Kalmbach implication.
mccune2 247 E2 - OL theorem proved by EQP
mccune3 248 E3 - OL theorem proved by EQP
i3n1 249 Equivalence for Kalmbach i...
ni31 250 Equivalence for Kalmbach i...
i3id 251 Identity for Kalmbach impl...
li3 252 Introduce Kalmbach implica...
ri3 253 Introduce Kalmbach implica...
2i3 254 Join both sides with Kalmb...
ud1lem0a 255 Introduce ` ->1 ` to the l...
ud1lem0b 256 Introduce ` ->1 ` to the r...
ud1lem0ab 257 Join both sides of hypothe...
ud2lem0a 258 Introduce ` ->2 ` to the l...
ud2lem0b 259 Introduce ` ->2 ` to the r...
ud3lem0a 260 Introduce Kalmbach implica...
ud3lem0b 261 Introduce Kalmbach implica...
ud4lem0a 262 Introduce ` ->4 ` to the l...
ud4lem0b 263 Introduce ` ->4 ` to the r...
ud5lem0a 264 Introduce ` ->5 ` to the l...
ud5lem0b 265 Introduce ` ->5 ` to the r...
i1i2 266 Correspondence between Sas...
i2i1 267 Correspondence between Sas...
i1i2con1 268 Correspondence between Sas...
i1i2con2 269 Correspondence between Sas...
i3i4 270 Correspondence between Kal...
i4i3 271 Correspondence between Kal...
i5con 272 Converse of ` ->5 ` .
0i1 273 Antecedent of 0 on Sasaki ...
1i1 274 Antecedent of 1 on Sasaki ...
i1id 275 Identity law for Sasaki co...
i2id 276 Identity law for Dishkant ...
ud1lem0c 277 Lemma for unified disjunct...
ud2lem0c 278 Lemma for unified disjunct...
ud3lem0c 279 Lemma for unified disjunct...
ud4lem0c 280 Lemma for unified disjunct...
ud5lem0c 281 Lemma for unified disjunct...
bina1 282 Pavicic binary logic ax-a1...
bina2 283 Pavicic binary logic ax-a2...
bina3 284 Pavicic binary logic ax-a3...
bina4 285 Pavicic binary logic ax-a4...
bina5 286 Pavicic binary logic ax-a5...
wql1lem 287 Classical implication infe...
wql2lem 288 Classical implication infe...
wql2lem2 289 Lemma for ` ->2 ` WQL axiom.
wql2lem3 290 Lemma for ` ->2 ` WQL axiom.
wql2lem4 291 Lemma for ` ->2 ` WQL axiom.
wql2lem5 292 Lemma for ` ->2 ` WQL axiom.
wql1 293 The 2nd hypothesis is the ...
oaidlem1 294 Lemma for OA identity-like...
womle2a 295 An equivalent to the WOM law.
womle2b 296 An equivalent to the WOM law.
womle3b 297 Implied by the WOM law.
womle 298 An equality implying the W...
nomb41 299 Lemma for "Non-Orthomodula...
nomb32 300 Lemma for "Non-Orthomodula...
nomcon0 301 Lemma for "Non-Orthomodula...
nomcon1 302 Lemma for "Non-Orthomodula...
nomcon2 303 Lemma for "Non-Orthomodula...
nomcon3 304 Lemma for "Non-Orthomodula...
nomcon4 305 Lemma for "Non-Orthomodula...
nomcon5 306 Lemma for "Non-Orthomodula...
nom10 307 Part of Lemma 3.3(14) from...
nom11 308 Part of Lemma 3.3(14) from...
nom12 309 Part of Lemma 3.3(14) from...
nom13 310 Part of Lemma 3.3(14) from...
nom14 311 Part of Lemma 3.3(14) from...
nom15 312 Part of Lemma 3.3(14) from...
nom20 313 Part of Lemma 3.3(14) from...
nom21 314 Part of Lemma 3.3(14) from...
nom22 315 Part of Lemma 3.3(14) from...
nom23 316 Part of Lemma 3.3(14) from...
nom24 317 Part of Lemma 3.3(14) from...
nom25 318 Part of Lemma 3.3(14) from...
nom30 319 Part of Lemma 3.3(14) from...
nom31 320 Part of Lemma 3.3(14) from...
nom32 321 Part of Lemma 3.3(14) from...
nom33 322 Part of Lemma 3.3(14) from...
nom34 323 Part of Lemma 3.3(14) from...
nom35 324 Part of Lemma 3.3(14) from...
nom40 325 Part of Lemma 3.3(15) from...
nom41 326 Part of Lemma 3.3(15) from...
nom42 327 Part of Lemma 3.3(15) from...
nom43 328 Part of Lemma 3.3(15) from...
nom44 329 Part of Lemma 3.3(15) from...
nom45 330 Part of Lemma 3.3(15) from...
nom50 331 Part of Lemma 3.3(15) from...
nom51 332 Part of Lemma 3.3(15) from...
nom52 333 Part of Lemma 3.3(15) from...
nom53 334 Part of Lemma 3.3(15) from...
nom54 335 Part of Lemma 3.3(15) from...
nom55 336 Part of Lemma 3.3(15) from...
nom60 337 Part of Lemma 3.3(15) from...
nom61 338 Part of Lemma 3.3(15) from...
nom62 339 Part of Lemma 3.3(15) from...
nom63 340 Part of Lemma 3.3(15) from...
nom64 341 Part of Lemma 3.3(15) from...
nom65 342 Part of Lemma 3.3(15) from...
go1 343 Lemma for proof of Mayet 8...
i2or 344 Lemma for disjunction of `...
i1or 345 Lemma for disjunction of `...
lei2 346 "Less than" analogue is eq...
i5lei1 347 Relevance implication is l...
i5lei2 348 Relevance implication is l...
i5lei3 349 Relevance implication is l...
i5lei4 350 Relevance implication is l...
id5leid0 351 Quantum identity is less t...
id5id0 352 Show that classical identi...
k1-6 353 Statement (6) in proof of ...
k1-7 354 Statement (7) in proof of ...
k1-8a 355 First part of statement (8...
k1-8b 356 Second part of statement (...
k1-2 357 Statement (2) in proof of ...
k1-3 358 Statement (3) in proof of ...
k1-4 359 Statement (4) in proof of ...
k1-5 360 Statement (5) in proof of ...
2vwomr2 362 2-variable WOML rule.
2vwomr1a 363 2-variable WOML rule.
2vwomr2a 364 2-variable WOML rule.
2vwomlem 365 Lemma from 2-variable WOML...
wr5-2v 366 WOML derived from 2-variab...
wom3 367 Weak orthomodular law for ...
wlor 368 Weak orthomodular law.
wran 369 Weak orthomodular law.
wlan 370 Weak orthomodular law.
wr2 371 Inference rule of AUQL.
w2or 372 Join both sides with disju...
w2an 373 Join both sides with conju...
w3tr1 374 Transitive inference usefu...
w3tr2 375 Transitive inference usefu...
wleoa 376 Relation between two metho...
wleao 377 Relation between two metho...
wdf-le1 378 Define 'less than or equal...
wdf-le2 379 Define 'less than or equal...
wom4 380 Orthomodular law. Kalmbac...
wom5 381 Orthomodular law. Kalmbac...
wcomlem 382 Analogue of commutation is...
wdf-c1 383 Show that commutator is a ...
wdf-c2 384 Show that commutator is a ...
wdf2le1 385 Alternate definition of 'l...
wdf2le2 386 Alternate definition of 'l...
wleo 387 L.e. absorption.
wlea 388 L.e. absorption.
wle1 389 Anything is l.e. 1.
wle0 390 0 is l.e. anything.
wler 391 Add disjunct to right of l.e.
wlel 392 Add conjunct to left of l.e.
wleror 393 Add disjunct to right of b...
wleran 394 Add conjunct to right of b...
wlecon 395 Contrapositive for l.e.
wletr 396 Transitive law for l.e.
wbltr 397 Transitive inference.
wlbtr 398 Transitive inference.
wle3tr1 399 Transitive inference usefu...
wle3tr2 400 Transitive inference usefu...
wbile 401 Biconditional to l.e.
wlebi 402 L.e. to biconditional.
wle2or 403 Disjunction of 2 l.e.'s.
wle2an 404 Conjunction of 2 l.e.'s.
wledi 405 Half of distributive law.
wledio 406 Half of distributive law.
wcom0 407 Commutation with 0. Kalmb...
wcom1 408 Commutation with 1. Kalmb...
wlecom 409 Comparable elements commut...
wbctr 410 Transitive inference.
wcbtr 411 Transitive inference.
wcomorr 412 Weak commutation law.
wcoman1 413 Weak commutation law.
wcomcom 414 Commutation is symmetric. ...
wcomcom2 415 Commutation equivalence. ...
wcomcom3 416 Commutation equivalence. ...
wcomcom4 417 Commutation equivalence. ...
wcomd 418 Commutation dual. Kalmbac...
wcom3ii 419 Lemma 3(ii) of Kalmbach 83...
wcomcom5 420 Commutation equivalence. ...
wcomdr 421 Commutation dual. Kalmbac...
wcom3i 422 Lemma 3(i) of Kalmbach 83 ...
wfh1 423 Weak structural analog of ...
wfh2 424 Weak structural analog of ...
wfh3 425 Weak structural analog of ...
wfh4 426 Weak structural analog of ...
wcom2or 427 Th. 4.2 Beran p. 49.
wcom2an 428 Th. 4.2 Beran p. 49.
wnbdi 429 Negated biconditional (dis...
wlem14 430 Lemma for KA14 soundness.
wr5 431 Proof of weak orthomodular...
ska2 432 Soundness theorem for Kalm...
ska4 433 Soundness theorem for Kalm...
wom2 434 Weak orthomodular law for ...
ka4ot 435 3-variable version of weak...
woml6 436 Variant of weakly orthomod...
woml7 437 Variant of weakly orthomod...
ortha 438 Property of orthogonality.
r3a 440 Orthomodular law restated.
wed 441 Weak equivalential detachm...
r3b 442 Orthomodular law from weak...
lem3.1 443 Lemma used in proof of Th....
lem3a.1 444 Lemma used in proof of Th....
oml 445 Orthomodular law. Compare...
omln 446 Orthomodular law.
omla 447 Orthomodular law.
omlan 448 Orthomodular law.
oml5 449 Orthomodular law.
oml5a 450 Orthomodular law.
oml2 451 Orthomodular law. Kalmbac...
oml3 452 Orthomodular law. Kalmbac...
comcom 453 Commutation is symmetric. ...
comcom3 454 Commutation equivalence. ...
comcom4 455 Commutation equivalence. ...
comd 456 Commutation dual. Kalmbac...
com3ii 457 Lemma 3(ii) of Kalmbach 83...
comcom5 458 Commutation equivalence. ...
comcom6 459 Commutation equivalence. ...
comcom7 460 Commutation equivalence. ...
comor1 461 Commutation law.
comor2 462 Commutation law.
comorr2 463 Commutation law.
comanr1 464 Commutation law.
comanr2 465 Commutation law.
comdr 466 Commutation dual. Kalmbac...
com3i 467 Lemma 3(i) of Kalmbach 83 ...
df2c1 468 Dual 'commutes' analogue f...
fh1 469 Foulis-Holland Theorem.
fh2 470 Foulis-Holland Theorem.
fh3 471 Foulis-Holland Theorem.
fh4 472 Foulis-Holland Theorem.
fh1r 473 Foulis-Holland Theorem.
fh2r 474 Foulis-Holland Theorem.
fh3r 475 Foulis-Holland Theorem.
fh4r 476 Foulis-Holland Theorem.
fh2c 477 Foulis-Holland Theorem.
fh4c 478 Foulis-Holland Theorem.
fh1rc 479 Foulis-Holland Theorem.
fh2rc 480 Foulis-Holland Theorem.
fh3rc 481 Foulis-Holland Theorem.
fh4rc 482 Foulis-Holland Theorem.
com2or 483 Th. 4.2 Beran p. 49.
com2an 484 Th. 4.2 Beran p. 49.
combi 485 Commutation theorem for Sa...
nbdi 486 Negated biconditional (dis...
oml4 487 Orthomodular law.
oml6 488 Orthomodular law.
gsth 489 Gudder-Schelp's Theorem. ...
gsth2 490 Stronger version of Gudder...
gstho 491 "OR" version of Gudder-Sch...
gt1 492 Part of Lemma 1 from Gaisi...
cmtr1com 493 Commutator equal to 1 comm...
comcmtr1 494 Commutation implies commut...
i0cmtrcom 495 Commutator element ` ->0 `...
i3bi 496 Kalmbach implication and b...
i3or 497 Kalmbach implication OR bu...
df2i3 498 Alternate definition for K...
dfi3b 499 Alternate Kalmbach conditi...
dfi4b 500 Alternate non-tollens cond...
i3n2 501 Equivalence for Kalmbach i...
ni32 502 Equivalence for Kalmbach i...
oi3ai3 503 Theorem for Kalmbach impli...
i3lem1 504 Lemma for Kalmbach implica...
i3lem2 505 Lemma for Kalmbach implica...
i3lem3 506 Lemma for Kalmbach implica...
i3lem4 507 Lemma for Kalmbach implica...
comi31 508 Commutation theorem.
com2i3 509 Commutation theorem.
comi32 510 Commutation theorem.
lem4 511 Lemma 4 of Kalmbach p. 240.
i0i3 512 Translation to Kalmbach im...
i3i0 513 Translation from Kalmbach ...
ska14 514 Soundness proof for KA14.
i3le 515 L.e. to Kalmbach implication.
bii3 516 Biconditional implies Kalm...
binr1 517 Pavicic binary logic ax-r1...
binr2 518 Pavicic binary logic ax-r2...
binr3 519 Pavicic binary logic axr3 ...
i31 520 Theorem for Kalmbach impli...
i3aa 521 Add antecedent.
i3abs1 522 Antecedent absorption.
i3abs2 523 Antecedent absorption.
i3abs3 524 Antecedent absorption.
i3orcom 525 Commutative law for conjun...
i3ancom 526 Commutative law for disjun...
bi3tr 527 Transitive inference.
i3btr 528 Transitive inference.
i33tr1 529 Transitive inference usefu...
i33tr2 530 Transitive inference usefu...
i3con1 531 Contrapositive.
i3ror 532 WQL (Weak Quantum Logic) r...
i3lor 533 WQL (Weak Quantum Logic) r...
i32or 534 WQL (Weak Quantum Logic) r...
i3ran 535 WQL (Weak Quantum Logic) r...
i3lan 536 WQL (Weak Quantum Logic) r...
i32an 537 WQL (Weak Quantum Logic) r...
i3ri3 538 WQL (Weak Quantum Logic) r...
i3li3 539 WQL (Weak Quantum Logic) r...
i32i3 540 WQL (Weak Quantum Logic) r...
i0i3tr 541 Transitive inference.
i3i0tr 542 Transitive inference.
i3th1 543 Theorem for Kalmbach impli...
i3th2 544 Theorem for Kalmbach impli...
i3th3 545 Theorem for Kalmbach impli...
i3th4 546 Theorem for Kalmbach impli...
i3th5 547 Theorem for Kalmbach impli...
i3th6 548 Theorem for Kalmbach impli...
i3th7 549 Theorem for Kalmbach impli...
i3th8 550 Theorem for Kalmbach impli...
i3con 551 Theorem for Kalmbach impli...
i3orlem1 552 Lemma for Kalmbach implica...
i3orlem2 553 Lemma for Kalmbach implica...
i3orlem3 554 Lemma for Kalmbach implica...
i3orlem4 555 Lemma for Kalmbach implica...
i3orlem5 556 Lemma for Kalmbach implica...
i3orlem6 557 Lemma for Kalmbach implica...
i3orlem7 558 Lemma for Kalmbach implica...
i3orlem8 559 Lemma for Kalmbach implica...
ud1lem1 560 Lemma for unified disjunct...
ud1lem2 561 Lemma for unified disjunct...
ud1lem3 562 Lemma for unified disjunct...
ud2lem1 563 Lemma for unified disjunct...
ud2lem2 564 Lemma for unified disjunct...
ud2lem3 565 Lemma for unified disjunct...
ud3lem1a 566 Lemma for unified disjunct...
ud3lem1b 567 Lemma for unified disjunct...
ud3lem1c 568 Lemma for unified disjunct...
ud3lem1d 569 Lemma for unified disjunct...
ud3lem1 570 Lemma for unified disjunct...
ud3lem2 571 Lemma for unified disjunct...
ud3lem3a 572 Lemma for unified disjunct...
ud3lem3b 573 Lemma for unified disjunct...
ud3lem3c 574 Lemma for unified disjunct...
ud3lem3d 575 Lemma for unified disjunct...
ud3lem3 576 Lemma for unified disjunct...
ud4lem1a 577 Lemma for unified disjunct...
ud4lem1b 578 Lemma for unified disjunct...
ud4lem1c 579 Lemma for unified disjunct...
ud4lem1d 580 Lemma for unified disjunct...
ud4lem1 581 Lemma for unified disjunct...
ud4lem2 582 Lemma for unified disjunct...
ud4lem3a 583 Lemma for unified disjunct...
ud4lem3b 584 Lemma for unified disjunct...
ud4lem3 585 Lemma for unified disjunct...
ud5lem1a 586 Lemma for unified disjunct...
ud5lem1b 587 Lemma for unified disjunct...
ud5lem1c 588 Lemma for unified disjunct...
ud5lem1 589 Lemma for unified disjunct...
ud5lem2 590 Lemma for unified disjunct...
ud5lem3a 591 Lemma for unified disjunct...
ud5lem3b 592 Lemma for unified disjunct...
ud5lem3c 593 Lemma for unified disjunct...
ud5lem3 594 Lemma for unified disjunct...
ud1 595 Unified disjunction for Sa...
ud2 596 Unified disjunction for Di...
ud3 597 Unified disjunction for Ka...
ud4 598 Unified disjunction for no...
ud5 599 Unified disjunction for re...
u1lemaa 600 Lemma for Sasaki implicati...
u2lemaa 601 Lemma for Dishkant implica...
u3lemaa 602 Lemma for Kalmbach implica...
u4lemaa 603 Lemma for non-tollens impl...
u5lemaa 604 Lemma for relevance implic...
u1lemana 605 Lemma for Sasaki implicati...
u2lemana 606 Lemma for Dishkant implica...
u3lemana 607 Lemma for Kalmbach implica...
u4lemana 608 Lemma for non-tollens impl...
u5lemana 609 Lemma for relevance implic...
u1lemab 610 Lemma for Sasaki implicati...
u2lemab 611 Lemma for Dishkant implica...
u3lemab 612 Lemma for Kalmbach implica...
u4lemab 613 Lemma for non-tollens impl...
u5lemab 614 Lemma for relevance implic...
u1lemanb 615 Lemma for Sasaki implicati...
u2lemanb 616 Lemma for Dishkant implica...
u3lemanb 617 Lemma for Kalmbach implica...
u4lemanb 618 Lemma for non-tollens impl...
u5lemanb 619 Lemma for relevance implic...
u1lemoa 620 Lemma for Sasaki implicati...
u2lemoa 621 Lemma for Dishkant implica...
u3lemoa 622 Lemma for Kalmbach implica...
u4lemoa 623 Lemma for non-tollens impl...
u5lemoa 624 Lemma for relevance implic...
u1lemona 625 Lemma for Sasaki implicati...
u2lemona 626 Lemma for Dishkant implica...
u3lemona 627 Lemma for Kalmbach implica...
u4lemona 628 Lemma for non-tollens impl...
u5lemona 629 Lemma for relevance implic...
u1lemob 630 Lemma for Sasaki implicati...
u2lemob 631 Lemma for Dishkant implica...
u3lemob 632 Lemma for Kalmbach implica...
u4lemob 633 Lemma for non-tollens impl...
u5lemob 634 Lemma for relevance implic...
u1lemonb 635 Lemma for Sasaki implicati...
u2lemonb 636 Lemma for Dishkant implica...
u3lemonb 637 Lemma for Kalmbach implica...
u4lemonb 638 Lemma for non-tollens impl...
u5lemonb 639 Lemma for relevance implic...
u1lemnaa 640 Lemma for Sasaki implicati...
u2lemnaa 641 Lemma for Dishkant implica...
u3lemnaa 642 Lemma for Kalmbach implica...
u4lemnaa 643 Lemma for non-tollens impl...
u5lemnaa 644 Lemma for relevance implic...
u1lemnana 645 Lemma for Sasaki implicati...
u2lemnana 646 Lemma for Dishkant implica...
u3lemnana 647 Lemma for Kalmbach implica...
u4lemnana 648 Lemma for non-tollens impl...
u5lemnana 649 Lemma for relevance implic...
u1lemnab 650 Lemma for Sasaki implicati...
u2lemnab 651 Lemma for Dishkant implica...
u3lemnab 652 Lemma for Kalmbach implica...
u4lemnab 653 Lemma for non-tollens impl...
u5lemnab 654 Lemma for relevance implic...
u1lemnanb 655 Lemma for Sasaki implicati...
u2lemnanb 656 Lemma for Dishkant implica...
u3lemnanb 657 Lemma for Kalmbach implica...
u4lemnanb 658 Lemma for non-tollens impl...
u5lemnanb 659 Lemma for relevance implic...
u1lemnoa 660 Lemma for Sasaki implicati...
u2lemnoa 661 Lemma for Dishkant implica...
u3lemnoa 662 Lemma for Kalmbach implica...
u4lemnoa 663 Lemma for non-tollens impl...
u5lemnoa 664 Lemma for relevance implic...
u1lemnona 665 Lemma for Sasaki implicati...
u2lemnona 666 Lemma for Dishkant implica...
u3lemnona 667 Lemma for Kalmbach implica...
u4lemnona 668 Lemma for non-tollens impl...
u5lemnona 669 Lemma for relevance implic...
u1lemnob 670 Lemma for Sasaki implicati...
u2lemnob 671 Lemma for Dishkant implica...
u3lemnob 672 Lemma for Kalmbach implica...
u4lemnob 673 Lemma for non-tollens impl...
u5lemnob 674 Lemma for relevance implic...
u1lemnonb 675 Lemma for Sasaki implicati...
u2lemnonb 676 Lemma for Dishkant implica...
u3lemnonb 677 Lemma for Kalmbach implica...
u4lemnonb 678 Lemma for non-tollens impl...
u5lemnonb 679 Lemma for relevance implic...
u1lemc1 680 Commutation theorem for Sa...
u2lemc1 681 Commutation theorem for Di...
u3lemc1 682 Commutation theorem for Ka...
u4lemc1 683 Commutation theorem for no...
u5lemc1 684 Commutation theorem for re...
u5lemc1b 685 Commutation theorem for re...
u1lemc2 686 Commutation theorem for Sa...
u2lemc2 687 Commutation theorem for Di...
u3lemc2 688 Commutation theorem for Ka...
u4lemc2 689 Commutation theorem for no...
u5lemc2 690 Commutation theorem for re...
u1lemc3 691 Commutation theorem for Sa...
u2lemc3 692 Commutation theorem for Di...
u3lemc3 693 Commutation theorem for Ka...
u4lemc3 694 Commutation theorem for no...
u5lemc3 695 Commutation theorem for re...
u1lemc5 696 Commutation theorem for Sa...
u2lemc5 697 Commutation theorem for Di...
u3lemc5 698 Commutation theorem for Ka...
u4lemc5 699 Commutation theorem for no...
u5lemc5 700 Commutation theorem for re...
u1lemc4 701 Lemma for Sasaki implicati...
u2lemc4 702 Lemma for Dishkant implica...
u3lemc4 703 Lemma for Kalmbach implica...
u4lemc4 704 Lemma for non-tollens impl...
u5lemc4 705 Lemma for relevance implic...
u1lemc6 706 Commutation theorem for Sa...
comi12 707 Commutation theorem for ` ...
i1com 708 Commutation expressed with...
comi1 709 Commutation expressed with...
u1lemle1 710 L.e. to Sasaki implication.
u2lemle1 711 L.e. to Dishkant implication.
u3lemle1 712 L.e. to Kalmbach implication.
u4lemle1 713 L.e. to non-tollens implic...
u5lemle1 714 L.e. to relevance implicat...
u1lemle2 715 Sasaki implication to l.e.
u2lemle2 716 Dishkant implication to l.e.
u3lemle2 717 Kalmbach implication to l.e.
u4lemle2 718 Non-tollens implication to...
u5lemle2 719 Relevance implication to l.e.
u1lembi 720 Sasaki implication and bic...
u2lembi 721 Dishkant implication and b...
i2bi 722 Dishkant implication expre...
u3lembi 723 Kalmbach implication and b...
u4lembi 724 Non-tollens implication an...
u5lembi 725 Relevance implication and ...
u12lembi 726 Sasaki/Dishkant implicatio...
u21lembi 727 Dishkant/Sasaki implicatio...
ublemc1 728 Commutation theorem for bi...
ublemc2 729 Commutation theorem for bi...
u1lemn1b 730 This theorem continues the...
u1lem3var1 731 A 3-variable formula. (Co...
oi3oa3lem1 732 An attempt at the OA3 conj...
oi3oa3 733 An attempt at the OA3 conj...
u1lem1 734 Lemma for unified implicat...
u2lem1 735 Lemma for unified implicat...
u3lem1 736 Lemma for unified implicat...
u4lem1 737 Lemma for unified implicat...
u5lem1 738 Lemma for unified implicat...
u1lem1n 739 Lemma for unified implicat...
u2lem1n 740 Lemma for unified implicat...
u3lem1n 741 Lemma for unified implicat...
u4lem1n 742 Lemma for unified implicat...
u5lem1n 743 Lemma for unified implicat...
u1lem2 744 Lemma for unified implicat...
u2lem2 745 Lemma for unified implicat...
u3lem2 746 Lemma for unified implicat...
u4lem2 747 Lemma for unified implicat...
u5lem2 748 Lemma for unified implicat...
u1lem3 749 Lemma for unified implicat...
u2lem3 750 Lemma for unified implicat...
u3lem3 751 Lemma for unified implicat...
u4lem3 752 Lemma for unified implicat...
u5lem3 753 Lemma for unified implicat...
u3lem3n 754 Lemma for unified implicat...
u4lem3n 755 Lemma for unified implicat...
u5lem3n 756 Lemma for unified implicat...
u1lem4 757 Lemma for unified implicat...
u3lem4 758 Lemma for unified implicat...
u4lem4 759 Lemma for unified implicat...
u5lem4 760 Lemma for unified implicat...
u1lem5 761 Lemma for unified implicat...
u2lem5 762 Lemma for unified implicat...
u3lem5 763 Lemma for unified implicat...
u4lem5 764 Lemma for unified implicat...
u5lem5 765 Lemma for unified implicat...
u4lem5n 766 Lemma for unified implicat...
u3lem6 767 Lemma for unified implicat...
u4lem6 768 Lemma for unified implicat...
u5lem6 769 Lemma for unified implicat...
u24lem 770 Lemma for unified implicat...
u12lem 771 Implication lemma.
u1lem7 772 Lemma for unified implicat...
u2lem7 773 Lemma for unified implicat...
u3lem7 774 Lemma for unified implicat...
u2lem7n 775 Lemma for unified implicat...
u1lem8 776 Lemma used in study of ort...
u1lem9a 777 Lemma used in study of ort...
u1lem9b 778 Lemma used in study of ort...
u1lem9ab 779 Lemma used in study of ort...
u1lem11 780 Lemma used in study of ort...
u1lem12 781 Lemma used in study of ort...
u2lem8 782 Lemma for unified implicat...
u3lem8 783 Lemma for unified implicat...
u3lem9 784 Lemma for unified implicat...
u3lem10 785 Lemma for unified implicat...
u3lem11 786 Lemma for unified implicat...
u3lem11a 787 Lemma for unified implicat...
u3lem12 788 Lemma for unified implicat...
u3lem13a 789 Lemma for unified implicat...
u3lem13b 790 Lemma for unified implicat...
u3lem14a 791 Lemma for unified implicat...
u3lem14aa 792 Used to prove ` ->1 ` "add...
u3lem14aa2 793 Used to prove ` ->1 ` "add...
u3lem14mp 794 Used to prove ` ->1 ` modu...
u3lem15 795 Lemma for Kalmbach implica...
u3lemax4 796 Possible axiom for Kalmbac...
u3lemax5 797 Possible axiom for Kalmbac...
bi1o1a 798 Equivalence to biconditional.
biao 799 Equivalence to biconditional.
i2i1i1 800 Equivalence to ` ->2 ` .
i1abs 801 An absorption law for ` ->...
test 802 Part of an attempt to crac...
test2 803 Part of an attempt to crac...
3vth1 804 A 3-variable theorem. Equ...
3vth2 805 A 3-variable theorem. Equ...
3vth3 806 A 3-variable theorem. Equ...
3vth4 807 A 3-variable theorem.
3vth5 808 A 3-variable theorem.
3vth6 809 A 3-variable theorem.
3vth7 810 A 3-variable theorem.
3vth8 811 A 3-variable theorem.
3vth9 812 A 3-variable theorem.
3vcom 813 3-variable commutation the...
3vded11 814 A 3-variable theorem. Exp...
3vded12 815 A 3-variable theorem. Exp...
3vded13 816 A 3-variable theorem. Exp...
3vded21 817 A 3-variable theorem. Exp...
3vded22 818 A 3-variable theorem. Exp...
3vded3 819 A 3-variable theorem. Exp...
1oa 820 Orthoarguesian-like law wi...
1oai1 821 Orthoarguesian-like OM law.
2oai1u 822 Orthoarguesian-like OM law.
1oaiii 823 OML analog to orthoarguesi...
1oaii 824 OML analog to orthoarguesi...
2oalem1 825 Lemma for OA-like stuff wi...
2oath1 826 OA-like theorem with ` ->2...
2oath1i1 827 Orthoarguesian-like OM law.
1oath1i1u 828 Orthoarguesian-like OM law.
oale 829 Relation for studying OA.
oaeqv 830 Weakened OA implies OA).
3vroa 831 OA-like inference rule (re...
mlalem 832 Lemma for Mladen's OML.
mlaoml 833 Mladen's OML.
eqtr4 834 4-variable transitive law ...
sac 835 Theorem showing "Sasaki co...
sa5 836 Possible axiom for a "Sasa...
salem1 837 Lemma for attempt at Sasak...
sadm3 838 Weak DeMorgan's law for at...
bi3 839 Chained biconditional.
bi4 840 Chained biconditional.
imp3 841 Implicational product with...
orbi 842 Disjunction of bicondition...
orbile 843 Disjunction of bicondition...
mlaconj4 844 For 4GO proof of Mladen's ...
mlaconj 845 For 5GO proof of Mladen's ...
mlaconj2 846 For 5GO proof of Mladen's ...
i1orni1 847 Complemented antecedent le...
negantlem1 848 Lemma for negated antecede...
negantlem2 849 Lemma for negated antecede...
negantlem3 850 Lemma for negated antecede...
negantlem4 851 Lemma for negated antecede...
negant 852 Negated antecedent identity.
negantlem5 853 Negated antecedent identity.
negantlem6 854 Negated antecedent identity.
negantlem7 855 Negated antecedent identity.
negantlem8 856 Negated antecedent identity.
negant0 857 Negated antecedent identity.
negant2 858 Negated antecedent identity.
negantlem9 859 Negated antecedent identity.
negant3 860 Negated antecedent identity.
negantlem10 861 Lemma for negated antecede...
negant4 862 Negated antecedent identity.
negant5 863 Negated antecedent identity.
neg3antlem1 864 Lemma for negated antecede...
neg3antlem2 865 Lemma for negated antecede...
neg3ant1 866 Lemma for negated antecede...
elimconslem 867 Lemma for consequent elimi...
elimcons 868 Consequent elimination law.
elimcons2 869 Consequent elimination law.
comanblem1 870 Lemma for biconditional co...
comanblem2 871 Lemma for biconditional co...
comanb 872 Biconditional commutation ...
comanbn 873 Biconditional commutation ...
mhlemlem1 874 Lemma for Lemma 7.1 of Kal...
mhlemlem2 875 Lemma for Lemma 7.1 of Kal...
mhlem 876 Lemma 7.1 of Kalmbach, p. 91.
mhlem1 877 Lemma for Marsden-Herman d...
mhlem2 878 Lemma for Marsden-Herman d...
mh 879 Marsden-Herman distributiv...
marsdenlem1 880 Lemma for Marsden-Herman d...
marsdenlem2 881 Lemma for Marsden-Herman d...
marsdenlem3 882 Lemma for Marsden-Herman d...
marsdenlem4 883 Lemma for Marsden-Herman d...
mh2 884 Marsden-Herman distributiv...
mlaconjolem 885 Lemma for OML proof of Mla...
mlaconjo 886 OML proof of Mladen's conj...
distid 887 Distributive law for ident...
mhcor1 888 Corollary of Marsden-Herma...
oago3.29 889 Equation (3.29) of "Equati...
oago3.21x 890 4-variable extension of Eq...
cancellem 891 Lemma for cancellation law...
cancel 892 Cancellation law eliminati...
kb10iii 893 Exercise 10(iii) of Kalmba...
e2ast2 894 Show that the E*_2 derivat...
e2astlem1 895 Lemma towards a possible p...
govar 896 Lemma for converting n-var...
govar2 897 Lemma for converting n-var...
gon2n 898 Lemma for converting n-var...
go2n4 899 8-variable Godowski equati...
gomaex4 900 Proof of Mayet Example 4 f...
go2n6 901 12-variable Godowski equat...
gomaex3h1 902 Hypothesis for Godowski 6-...
gomaex3h2 903 Hypothesis for Godowski 6-...
gomaex3h3 904 Hypothesis for Godowski 6-...
gomaex3h4 905 Hypothesis for Godowski 6-...
gomaex3h5 906 Hypothesis for Godowski 6-...
gomaex3h6 907 Hypothesis for Godowski 6-...
gomaex3h7 908 Hypothesis for Godowski 6-...
gomaex3h8 909 Hypothesis for Godowski 6-...
gomaex3h9 910 Hypothesis for Godowski 6-...
gomaex3h10 911 Hypothesis for Godowski 6-...
gomaex3h11 912 Hypothesis for Godowski 6-...
gomaex3h12 913 Hypothesis for Godowski 6-...
gomaex3lem1 914 Lemma for Godowski 6-var -...
gomaex3lem2 915 Lemma for Godowski 6-var -...
gomaex3lem3 916 Lemma for Godowski 6-var -...
gomaex3lem4 917 Lemma for Godowski 6-var -...
gomaex3lem5 918 Lemma for Godowski 6-var -...
gomaex3lem6 919 Lemma for Godowski 6-var -...
gomaex3lem7 920 Lemma for Godowski 6-var -...
gomaex3lem8 921 Lemma for Godowski 6-var -...
gomaex3lem9 922 Lemma for Godowski 6-var -...
gomaex3lem10 923 Lemma for Godowski 6-var -...
gomaex3 924 Proof of Mayet Example 3 f...
oas 925 "Strengthening" lemma for ...
oasr 926 Reverse of ~ oas lemma for...
oat 927 Transformation lemma for s...
oatr 928 Reverse transformation lem...
oau 929 Transformation lemma for s...
oaur 930 Transformation lemma for s...
oaidlem2 931 Lemma for identity-like OA...
oaidlem2g 932 Lemma for identity-like OA...
oa6v4v 933 6-variable OA to 4-variabl...
oa4v3v 934 4-variable OA to 3-variabl...
oal42 935 Derivation of Godowski/Gre...
oa23 936 Derivation of OA from Godo...
oa4lem1 937 Lemma for 3-var to 4-var OA.
oa4lem2 938 Lemma for 3-var to 4-var OA.
oa4lem3 939 Lemma for 3-var to 4-var OA.
distoah1 940 Satisfaction of distributi...
distoah2 941 Satisfaction of distributi...
distoah3 942 Satisfaction of distributi...
distoah4 943 Satisfaction of distributi...
distoa 944 Derivation in OM of OA, as...
oa3to4lem1 945 Lemma for orthoarguesian l...
oa3to4lem2 946 Lemma for orthoarguesian l...
oa3to4lem3 947 Lemma for orthoarguesian l...
oa3to4lem4 948 Lemma for orthoarguesian l...
oa3to4lem5 949 Lemma for orthoarguesian l...
oa3to4lem6 950 Orthoarguesian law (Godows...
oa3to4 951 Orthoarguesian law (Godows...
oa6todual 952 Conventional to dual 6-var...
oa6fromdual 953 Dual to conventional 6-var...
oa6fromdualn 954 Dual to conventional 6-var...
oa6to4h1 955 Satisfaction of 6-variable...
oa6to4h2 956 Satisfaction of 6-variable...
oa6to4h3 957 Satisfaction of 6-variable...
oa6to4 958 Derivation of 4-variable p...
oa4b 959 Derivation of 4-OA law var...
oa4to6lem1 960 Lemma for orthoarguesian l...
oa4to6lem2 961 Lemma for orthoarguesian l...
oa4to6lem3 962 Lemma for orthoarguesian l...
oa4to6lem4 963 Lemma for orthoarguesian l...
oa4to6dual 964 Lemma for orthoarguesian l...
oa4to6 965 Orthoarguesian law (4-vari...
oa4btoc 966 Derivation of 4-OA law var...
oa4ctob 967 Derivation of 4-OA law var...
oa4ctod 968 Derivation of 4-OA law var...
oa4dtoc 969 Derivation of 4-OA law var...
oa4dcom 970 Lemma commuting terms.
oa8todual 971 Conventional to dual 8-var...
oa8to5 972 Orthoarguesian law 5OA con...
oa4to4u 973 A "universal" 4-OA. The hy...
oa4to4u2 974 A weaker-looking "universa...
oa4uto4g 975 Derivation of "Godowski/Gr...
oa4gto4u 976 A "universal" 4-OA derived...
oa4uto4 977 Derivation of standard 4-v...
oa3-2lema 978 Lemma for 3-OA(2). Equiva...
oa3-2lemb 979 Lemma for 3-OA(2). Equiva...
oa3-6lem 980 Lemma for 3-OA(6). Equiva...
oa3-3lem 981 Lemma for 3-OA(3). Equiva...
oa3-1lem 982 Lemma for 3-OA(1). Equiva...
oa3-4lem 983 Lemma for 3-OA(4). Equiva...
oa3-5lem 984 Lemma for 3-OA(5). Equiva...
oa3-u1lem 985 Lemma for a "universal" 3-...
oa3-u2lem 986 Lemma for a "universal" 3-...
oa3-6to3 987 Derivation of 3-OA variant...
oa3-2to4 988 Derivation of 3-OA variant...
oa3-2wto2 989 Derivation of 3-OA variant...
oa3-2to2s 990 Derivation of 3-OA variant...
oa3-u1 991 Derivation of a "universal...
oa3-u2 992 Derivation of a "universal...
oa3-1to5 993 Derivation of an equivalen...
d3oa 995 Derivation of 3-OA from OA...
d4oa 996 Variant of proper 4-OA pro...
d6oa 997 Derivation of 6-variable o...
oal2 999 Orthoarguesian law - ` ->2...
oal1 1000 Orthoarguesian law - ` ->1...
oaliii 1001 Orthoarguesian law. Godow...
oalii 1002 Orthoarguesian law. Godow...
oaliv 1003 Orthoarguesian law. Godow...
oath1 1004 OA theorem.
oalem1 1005 Lemma.
oalem2 1006 Lemma.
oadist2a 1007 Distributive inference der...
oadist2b 1008 Distributive inference der...
oadist2 1009 Distributive inference der...
oadist12 1010 Distributive law derived f...
oacom 1011 Commutation law requiring OA.
oacom2 1012 Commutation law requiring OA.
oacom3 1013 Commutation law requiring OA.
oagen1 1014 "Generalized" OA.
oagen1b 1015 "Generalized" OA.
oagen2 1016 "Generalized" OA.
oagen2b 1017 "Generalized" OA.
mloa 1018 Mladen's OA
oadist 1019 Distributive law derived f...
oadistb 1020 Distributive law derived f...
oadistc0 1021 Pre-distributive law.
oadistc 1022 Distributive law.
oadistd 1023 OA distributive law.
3oa2 1024 Alternate form for the 3-v...
3oa3 1025 3-variable orthoarguesion ...
oa4cl 1027 4-variable OA closed equat...
oa43v 1028 Derivation of 3-variable O...
oa3moa3 1029 4-variable 3OA to 5-variab...
oa64v 1031 Derivation of 4-variable O...
oa63v 1032 Derivation of 3-variable O...
axoa4 1034 The proper 4-variable OA law.
axoa4b 1035 Proper 4-variable OA law v...
oa6 1036 Derivation of 6-variable o...
axoa4a 1037 Proper 4-variable OA law v...
axoa4d 1038 Proper 4-variable OA law v...
4oa 1039 Variant of proper 4-OA.
4oaiii 1040 Proper OA analog to Godows...
4oath1 1041 Proper 4-OA theorem.
4oagen1 1042 "Generalized" 4-OA.
4oagen1b 1043 "Generalized" OA.
4oadist 1044 OA Distributive law. This...
lem3.3.2 1046 Equation 3.2 of [PavMeg199...
lem3.3.3lem1 1049 Lemma for ~ lem3.3.3 .
lem3.3.3lem2 1050 Lemma for ~ lem3.3.3 .
lem3.3.3lem3 1051 Lemma for ~ lem3.3.3 .
lem3.3.3 1052 Equation 3.3 of [PavMeg199...
lem3.3.4 1053 Equation 3.4 of [PavMeg199...
lem3.3.5lem 1054 A fundamental property in ...
lem3.3.5 1055 Equation 3.5 of [PavMeg199...
lem3.3.6 1056 Equation 3.6 of [PavMeg199...
lem3.3.7i0e1 1057 Equation 3.7 of [PavMeg199...
lem3.3.7i0e2 1058 Equation 3.7 of [PavMeg199...
lem3.3.7i0e3 1059 Equation 3.7 of [PavMeg199...
lem3.3.7i1e1 1060 Equation 3.7 of [PavMeg199...
lem3.3.7i1e2 1061 Equation 3.7 of [PavMeg199...
lem3.3.7i1e3 1062 Equation 3.7 of [PavMeg199...
lem3.3.7i2e1 1063 Equation 3.7 of [PavMeg199...
lem3.3.7i2e2 1064 Equation 3.7 of [PavMeg199...
lem3.3.7i2e3 1065 Equation 3.7 of [PavMeg199...
lem3.3.7i3e1 1066 Equation 3.7 of [PavMeg199...
lem3.3.7i3e2 1067 Equation 3.7 of [PavMeg199...
lem3.3.7i3e3 1068 Equation 3.7 of [PavMeg199...
lem3.3.7i4e1 1069 Equation 3.7 of [PavMeg199...
lem3.3.7i4e2 1070 Equation 3.7 of [PavMeg199...
lem3.3.7i4e3 1071 Equation 3.7 of [PavMeg199...
lem3.3.7i5e1 1072 Equation 3.7 of [PavMeg199...
lem3.3.7i5e2 1073 Equation 3.7 of [PavMeg199...
lem3.3.7i5e3 1074 Equation 3.7 of [PavMeg199...
lem3.4.1 1075 Equation 3.9 of [PavMeg199...
lem3.4.3 1076 Equation 3.11 of [PavMeg19...
lem3.4.4 1077 Equation 3.12 of [PavMeg19...
lem3.4.5 1078 Equation 3.13 of [PavMeg19...
lem3.4.6 1079 Equation 3.14 of [PavMeg19...
lem4.6.2e1 1080 Equation 4.10 of [MegPav20...
lem4.6.2e2 1081 Equation 4.10 of [MegPav20...
lem4.6.3le1 1082 Equation 4.11 of [MegPav20...
lem4.6.3le2 1083 Equation 4.11 of [MegPav20...
lem4.6.4 1084 Equation 4.12 of [MegPav20...
lem4.6.5 1085 Equation 4.13 of [MegPav20...
lem4.6.6i0j1 1086 Equation 4.14 of [MegPav20...
lem4.6.6i0j2 1087 Equation 4.14 of [MegPav20...
lem4.6.6i0j3 1088 Equation 4.14 of [MegPav20...
lem4.6.6i0j4 1089 Equation 4.14 of [MegPav20...
lem4.6.6i1j0 1090 Equation 4.14 of [MegPav20...
lem4.6.6i1j2 1091 Equation 4.14 of [MegPav20...
lem4.6.6i1j3 1092 Equation 4.14 of [MegPav20...
lem4.6.6i2j0 1093 Equation 4.14 of [MegPav20...
lem4.6.6i2j1 1094 Equation 4.14 of [MegPav20...
lem4.6.6i2j4 1095 Equation 4.14 of [MegPav20...
lem4.6.6i3j0 1096 Equation 4.14 of [MegPav20...
lem4.6.6i3j1 1097 Equation 4.14 of [MegPav20...
lem4.6.6i4j0 1098 Equation 4.14 of [MegPav20...
lem4.6.6i4j2 1099 Equation 4.14 of [MegPav20...
com3iia 1100 The dual of ~ com3ii . (C...
lem4.6.7 1101 Equation 4.15 of [MegPav20...
wdcom 1103 Any two variables (weakly)...
wdwom 1104 Prove 2-variable WOML rule...
wddi1 1105 Prove the weak distributiv...
wddi2 1106 The weak distributive law ...
wddi3 1107 The weak distributive law ...
wddi4 1108 The weak distributive law ...
wdid0id5 1109 Show that quantum identity...
wdid0id1 1110 Show a quantum identity th...
wdid0id2 1111 Show a quantum identity th...
wdid0id3 1112 Show a quantum identity th...
wdid0id4 1113 Show a quantum identity th...
wdka4o 1114 Show WDOL analog of WOM law.
wddi-0 1115 The weak distributive law ...
wddi-1 1116 The weak distributive law ...
wddi-2 1117 The weak distributive law ...
wddi-3 1118 The weak distributive law ...
wddi-4 1119 The weak distributive law ...
ml 1121 Modular law in equational ...
mldual 1122 Dual of modular law.
ml2i 1123 Inference version of modul...
mli 1124 Inference version of modul...
mldual2i 1125 Inference version of dual ...
mlduali 1126 Inference version of dual ...
ml3le 1127 Form of modular law that s...
ml3 1128 Form of modular law that s...
vneulem1 1129 Part of von Neumann's lemm...
vneulem2 1130 Part of von Neumann's lemm...
vneulem3 1131 Part of von Neumann's lemm...
vneulem4 1132 Part of von Neumann's lemm...
vneulem5 1133 Part of von Neumann's lemm...
vneulem6 1134 Part of von Neumann's lemm...
vneulem7 1135 Part of von Neumann's lemm...
vneulem8 1136 Part of von Neumann's lemm...
vneulem9 1137 Part of von Neumann's lemm...
vneulem10 1138 Part of von Neumann's lemm...
vneulem11 1139 Part of von Neumann's lemm...
vneulem12 1140 Part of von Neumann's lemm...
vneulem13 1141 Part of von Neumann's lemm...
vneulem14 1142 Part of von Neumann's lemm...
vneulem15 1143 Part of von Neumann's lemm...
vneulem16 1144 Part of von Neumann's lemm...
vneulem 1145 von Neumann's modular law ...
vneulemexp 1146 Expanded version of ~ vneu...
l42modlem1 1147 Lemma for ~ l42mod ..
l42modlem2 1148 Lemma for ~ l42mod ..
l42mod 1149 An equation that fails in ...
modexp 1150 Expansion by modular law.
dp15lema 1152 Part of proof (1)=>(5) in ...
dp15lemb 1153 Part of proof (1)=>(5) in ...
dp15lemc 1154 Part of proof (1)=>(5) in ...
dp15lemd 1155 Part of proof (1)=>(5) in ...
dp15leme 1156 Part of proof (1)=>(5) in ...
dp15lemf 1157 Part of proof (1)=>(5) in ...
dp15lemg 1158 Part of proof (1)=>(5) in ...
dp15lemh 1159 Part of proof (1)=>(5) in ...
dp15 1160 Part of theorem from Alan ...
dp53lema 1161 Part of proof (5)=>(3) in ...
dp53lemb 1162 Part of proof (5)=>(3) in ...
dp53lemc 1163 Part of proof (5)=>(3) in ...
dp53lemd 1164 Part of proof (5)=>(3) in ...
dp53leme 1165 Part of proof (5)=>(3) in ...
dp53lemf 1166 Part of proof (5)=>(3) in ...
dp53lemg 1167 Part of proof (5)=>(3) in ...
dp53 1168 Part of theorem from Alan ...
dp35lemg 1169 Part of proof (3)=>(5) in ...
dp35lemf 1170 Part of proof (3)=>(5) in ...
dp35leme 1171 Part of proof (3)=>(5) in ...
dp35lemd 1172 Part of proof (3)=>(5) in ...
dp35lemc 1173 Part of proof (3)=>(5) in ...
dp35lemb 1174 Part of proof (3)=>(5) in ...
dp35lembb 1175 Part of proof (3)=>(5) in ...
dp35lema 1176 Part of proof (3)=>(5) in ...
dp35lem0 1177 Part of proof (3)=>(5) in ...
dp35 1178 Part of theorem from Alan ...
dp34 1179 Part of theorem from Alan ...
dp41lema 1180 Part of proof (4)=>(1) in ...
dp41lemb 1181 Part of proof (4)=>(1) in ...
dp41lemc0 1182 Part of proof (4)=>(1) in ...
dp41lemc 1183 Part of proof (4)=>(1) in ...
dp41lemd 1184 Part of proof (4)=>(1) in ...
dp41leme 1185 Part of proof (4)=>(1) in ...
dp41lemf 1186 Part of proof (4)=>(1) in ...
dp41lemg 1187 Part of proof (4)=>(1) in ...
dp41lemh 1188 Part of proof (4)=>(1) in ...
dp41lemj 1189 Part of proof (4)=>(1) in ...
dp41lemk 1190 Part of proof (4)=>(1) in ...
dp41leml 1191 Part of proof (4)=>(1) in ...
dp41lemm 1192 Part of proof (4)=>(1) in ...
dp41 1193 Part of theorem from Alan ...
dp32 1194 Part of theorem from Alan ...
dp23 1195 Part of theorem from Alan ...
xdp41 1196 Part of proof (4)=>(1) in ...
xdp15 1197 Part of proof (1)=>(5) in ...
xdp53 1198 Part of proof (5)=>(3) in ...
xxdp41 1199 Part of proof (4)=>(1) in ...
xxdp15 1200 Part of proof (1)=>(5) in ...
xxdp53 1201 Part of proof (5)=>(3) in ...
xdp45lem 1202 Part of proof (4)=>(5) in ...
xdp43lem 1203 Part of proof (4)=>(3) in ...
xdp45 1204 Part of proof (4)=>(5) in ...
xdp43 1205 Part of proof (4)=>(3) in ...
3dp43 1206 "3OA" version of ~ xdp43 ....
oadp35lemg 1207 Part of proof (3)=>(5) in ...
oadp35lemf 1208 Part of proof (3)=>(5) in ...
oadp35lemc 1209 Part of proof (3)=>(5) in ...
oadp35 1210 Part of theorem from Alan ...
testmod 1211 A modular law experiment.
testmod1 1212 A modular law experiment.
testmod2 1213 A modular law experiment.
testmod2expanded 1214 A modular law experiment.
testmod3 1215 A modular law experiment.
  Copyright terms: Public domain W3C validator