List of Theorems|
Ref | Description
|
| id 59 |
Identity law. (Contribute... |
| 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 inferenc... |
| 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. (Contrib... |
| ancom 74 |
Commutative law. (Contrib... |
| orass 75 |
Associative law. (Contrib... |
| anass 76 |
Associative law. (Contrib... |
| lan 77 |
Introduce conjunct on left... |
| ran 78 |
Introduce conjunct on righ... |
| 2an 79 |
Conjoin both sides of hypo... |
| or12 80 |
Swap disjuncts. (Contribu... |
| an12 81 |
Swap conjuncts. (Contribu... |
| or32 82 |
Swap disjuncts. (Contribu... |
| an32 83 |
Swap conjuncts. (Contribu... |
| or4 84 |
Swap disjuncts. (Contribu... |
| or42 85 |
Rearrange disjuncts. (Con... |
| an4 86 |
Swap conjuncts. (Contribu... |
| 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. (C... |
| bicom 96 |
Commutative law. (Contrib... |
| lbi 97 |
Introduce biconditional to... |
| rbi 98 |
Introduce biconditional to... |
| 2bi 99 |
Join both sides with bicon... |
| dff2 100 |
Alternate definition of "f... |
| dff 101 |
Alternate definition of "f... |
| or0 102 |
Disjunction with 0. (Cont... |
| or0r 103 |
Disjunction with 0. (Cont... |
| or1 104 |
Disjunction with 1. (Cont... |
| or1r 105 |
Disjunction with 1. (Cont... |
| an1 106 |
Conjunction with 1. (Cont... |
| an1r 107 |
Conjunction with 1. (Cont... |
| an0 108 |
Conjunction with 0. (Cont... |
| an0r 109 |
Conjunction with 0. (Cont... |
| oridm 110 |
Idempotent law. (Contribu... |
| anidm 111 |
Idempotent law. (Contribu... |
| orordi 112 |
Distribution of disjunctio... |
| orordir 113 |
Distribution of disjunctio... |
| anandi 114 |
Distribution of conjunctio... |
| anandir 115 |
Distribution of conjunctio... |
| biid 116 |
Identity law. (Contribute... |
| 1b 117 |
Identity law. (Contribute... |
| bi1 118 |
Identity inference. (Cont... |
| 1bi 119 |
Identity inference. (Cont... |
| orabs 120 |
Absorption law. (Contribu... |
| anabs 121 |
Absorption law. (Contribu... |
| conb 122 |
Contraposition law. (Cont... |
| leoa 123 |
Relation between two metho... |
| leao 124 |
Relation between two metho... |
| mi 125 |
Mittelstaedt implication. ... |
| di 126 |
Dishkant implication. (Co... |
| omlem1 127 |
Lemma in proof of Thm. 1 o... |
| omlem2 128 |
Lemma in proof of Thm. 1 o... |
| df2le1 135 |
Alternate definition of "l... |
| df2le2 136 |
Alternate definition of "l... |
| letr 137 |
Transitive law for "less t... |
| bltr 138 |
Transitive inference. (Co... |
| lbtr 139 |
Transitive inference. (Co... |
| le3tr1 140 |
Transitive inference usefu... |
| le3tr2 141 |
Transitive inference usefu... |
| bile 142 |
Biconditional to "less tha... |
| qlhoml1a 143 |
An ortholattice inequality... |
| qlhoml1b 144 |
An ortholattice inequality... |
| lebi 145 |
"Less than or equal to" to... |
| le1 146 |
Anything is less than or e... |
| le0 147 |
0 is less than or equal to... |
| leid 148 |
Identity law for "less tha... |
| ler 149 |
Add disjunct to right of l... |
| lerr 150 |
Add disjunct to right of l... |
| lel 151 |
Add conjunct to left of l.... |
| 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. (Contrib... |
| leor 159 |
L.e. absorption. (Contrib... |
| lea 160 |
L.e. absorption. (Contrib... |
| lear 161 |
L.e. absorption. (Contrib... |
| leao1 162 |
L.e. absorption. (Contrib... |
| leao2 163 |
L.e. absorption. (Contrib... |
| leao3 164 |
L.e. absorption. (Contrib... |
| leao4 165 |
L.e. absorption. (Contrib... |
| 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. (Co... |
| cbtr 182 |
Transitive inference. (Co... |
| 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. (Cont... |
| cmtrcom 190 |
Commutative law for commut... |
| wa1 191 |
Weak A1. (Contributed by ... |
| wa2 192 |
Weak A2. (Contributed by ... |
| wa3 193 |
Weak A3. (Contributed by ... |
| wa4 194 |
Weak A4. (Contributed by ... |
| wa5 195 |
Weak A5. (Contributed by ... |
| wa6 196 |
Weak A6. (Contributed by ... |
| wr1 197 |
Weak R1. (Contributed by ... |
| wr3 198 |
Weak R3. (Contributed by ... |
| wr4 199 |
Weak R4. (Contributed by ... |
| wa5b 200 |
Absorption law. (Contribu... |
| wa5c 201 |
Absorption law. (Contribu... |
| wcon 202 |
Contraposition law. (Cont... |
| wancom 203 |
Commutative law. (Contrib... |
| wanass 204 |
Associative law. (Contrib... |
| wwbmp 205 |
Weak weak equivalential de... |
| wwbmpr 206 |
Weak weak equivalential de... |
| wcon1 207 |
Weak contraposition. (Con... |
| wcon2 208 |
Weak contraposition. (Con... |
| wcon3 209 |
Weak contraposition. (Con... |
| wlem3.1 210 |
Weak analogue to lemma use... |
| woml 211 |
Theorem structurally simil... |
| wwoml2 212 |
Weak orthomodular law. (C... |
| wwoml3 213 |
Weak orthomodular law. (C... |
| 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. (Contrib... |
| 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 implicati... |
| mccune2 247 |
E2 - OL theorem proved by ... |
| mccune3 248 |
E3 - OL theorem proved by ... |
| 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 ` . (Co... |
| 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 axio... |
| wql2lem3 290 |
Lemma for ` ->2 ` WQL axio... |
| wql2lem4 291 |
Lemma for ` ->2 ` WQL axio... |
| wql2lem5 292 |
Lemma for ` ->2 ` WQL axio... |
| wql1 293 |
The 2nd hypothesis is the ... |
| oaidlem1 294 |
Lemma for OA identity-like... |
| womle2a 295 |
An equivalent to the WOM l... |
| womle2b 296 |
An equivalent to the WOM l... |
| 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. (Co... |
| 2vwomr1a 363 |
2-variable WOML rule. (Co... |
| 2vwomr2a 364 |
2-variable WOML rule. (Co... |
| 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. (C... |
| wran 369 |
Weak orthomodular law. (C... |
| wlan 370 |
Weak orthomodular law. (C... |
| wr2 371 |
Inference rule of AUQL. (C... |
| 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. (Contrib... |
| wlea 388 |
L.e. absorption. (Contrib... |
| wle1 389 |
Anything is less than or e... |
| wle0 390 |
0 is less than or equal to... |
| wler 391 |
Add disjunct to right of l... |
| wlel 392 |
Add conjunct to left of l.... |
| 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. (Co... |
| wlbtr 398 |
Transitive inference. (Co... |
| wle3tr1 399 |
Transitive inference usefu... |
| wle3tr2 400 |
Transitive inference usefu... |
| wbile 401 |
Biconditional to l.e. (Co... |
| wlebi 402 |
L.e. to biconditional. (C... |
| 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. (Co... |
| wcbtr 411 |
Transitive inference. (Co... |
| wcomorr 412 |
Weak commutation law. (Co... |
| wcoman1 413 |
Weak commutation law. (Co... |
| 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 |
Thm. 4.2 Beran p. 49. (Co... |
| wcom2an 428 |
Thm. 4.2 Beran p. 49. (Co... |
| 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 Thm... |
| lem3a.1 444 |
Lemma used in proof of Thm... |
| oml 445 |
Orthomodular law. Compare... |
| omln 446 |
Orthomodular law. (Contri... |
| omla 447 |
Orthomodular law. (Contri... |
| omlan 448 |
Orthomodular law. (Contri... |
| oml5 449 |
Orthomodular law. (Contri... |
| oml5a 450 |
Orthomodular law. (Contri... |
| 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. (Contrib... |
| comor2 462 |
Commutation law. (Contrib... |
| comorr2 463 |
Commutation law. (Contrib... |
| comanr1 464 |
Commutation law. (Contrib... |
| comanr2 465 |
Commutation law. (Contrib... |
| 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 |
Thm. 4.2 Beran p. 49. (Co... |
| com2an 484 |
Thm. 4.2 Beran p. 49. (Co... |
| combi 485 |
Commutation theorem for Sa... |
| nbdi 486 |
Negated biconditional (dis... |
| oml4 487 |
Orthomodular law. (Contri... |
| oml6 488 |
Orthomodular law. (Contri... |
| 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. (Con... |
| com2i3 509 |
Commutation theorem. (Con... |
| comi32 510 |
Commutation theorem. (Con... |
| 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 implicati... |
| bii3 516 |
Biconditional implies Kalm... |
| binr1 517 |
Pavicic binary logic ~ ax-... |
| binr2 518 |
Pavicic binary logic ~ ax-... |
| binr3 519 |
Pavicic binary logic ~ ax-... |
| i31 520 |
Theorem for Kalmbach impli... |
| i3aa 521 |
Add antecedent. (Contribu... |
| i3abs1 522 |
Antecedent absorption. (C... |
| i3abs2 523 |
Antecedent absorption. (C... |
| i3abs3 524 |
Antecedent absorption. (C... |
| i3orcom 525 |
Commutative law for conjun... |
| i3ancom 526 |
Commutative law for disjun... |
| bi3tr 527 |
Transitive inference. (Co... |
| i3btr 528 |
Transitive inference. (Co... |
| i33tr1 529 |
Transitive inference usefu... |
| i33tr2 530 |
Transitive inference usefu... |
| i3con1 531 |
Contrapositive. (Contribu... |
| 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. (Co... |
| i3i0tr 542 |
Transitive inference. (Co... |
| 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 implicati... |
| u3lemle1 712 |
L.e. to Kalmbach implicati... |
| 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.... |
| u3lemle2 717 |
Kalmbach implication to l.... |
| u4lemle2 718 |
Non-tollens implication to... |
| u5lemle2 719 |
Relevance implication to l... |
| 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. (Contr... |
| 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 bicondition... |
| biao 799 |
Equivalence to bicondition... |
| 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. (Co... |
| 3vth5 808 |
A 3-variable theorem. (Co... |
| 3vth6 809 |
A 3-variable theorem. (Co... |
| 3vth7 810 |
A 3-variable theorem. (Co... |
| 3vth8 811 |
A 3-variable theorem. (Co... |
| 3vth9 812 |
A 3-variable theorem. (Co... |
| 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. (C... |
| mlaoml 833 |
Mladen's OML. (Contributed... |
| 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. (C... |
| bi4 840 |
Chained biconditional. (C... |
| 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 identit... |
| negantlem5 853 |
Negated antecedent identit... |
| negantlem6 854 |
Negated antecedent identit... |
| negantlem7 855 |
Negated antecedent identit... |
| negantlem8 856 |
Negated antecedent identit... |
| negant0 857 |
Negated antecedent identit... |
| negant2 858 |
Negated antecedent identit... |
| negantlem9 859 |
Negated antecedent identit... |
| negant3 860 |
Negated antecedent identit... |
| negantlem10 861 |
Lemma for negated antecede... |
| negant4 862 |
Negated antecedent identit... |
| negant5 863 |
Negated antecedent identit... |
| 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. ... |
| 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 O... |
| oa4lem2 938 |
Lemma for 3-var to 4-var O... |
| oa4lem3 939 |
Lemma for 3-var to 4-var O... |
| 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. (C... |
| 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. (Contributed ... |
| oalem1 1005 |
Lemma. (Contributed by NM... |
| oalem2 1006 |
Lemma. (Contributed by NM... |
| 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 ... |
| oacom2 1012 |
Commutation law requiring ... |
| oacom3 1013 |
Commutation law requiring ... |
| oagen1 1014 |
"Generalized" OA. (Contrib... |
| oagen1b 1015 |
"Generalized" OA. (Contrib... |
| oagen2 1016 |
"Generalized" OA. (Contrib... |
| oagen2b 1017 |
"Generalized" OA. (Contrib... |
| mloa 1018 |
Mladen's OA. (Contributed ... |
| oadist 1019 |
Distributive law derived f... |
| oadistb 1020 |
Distributive law derived f... |
| oadistc0 1021 |
Pre-distributive law. Not... |
| oadistc 1022 |
Distributive law. (Contri... |
| oadistd 1023 |
OA distributive law. (Con... |
| 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 l... |
| 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. (C... |
| 4oaiii 1040 |
Proper OA analog to Godows... |
| 4oath1 1041 |
Proper 4-OA theorem. (Con... |
| 4oagen1 1042 |
"Generalized" 4-OA. (Contr... |
| 4oagen1b 1043 |
"Generalized" OA. (Contrib... |
| 4oadist 1044 |
OA Distributive law. This... |
| lem3.3.2 1046 |
Equation 3.2 of [PavMeg199... |
| lem3.3.3lem1 1049 |
Lemma for ~ lem3.3.3 . (C... |
| lem3.3.3lem2 1050 |
Lemma for ~ lem3.3.3 . (C... |
| lem3.3.3lem3 1051 |
Lemma for ~ lem3.3.3 . (C... |
| 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... |
| thm3.8i1lem 1080 |
Lemma intended for ~~ thm3... |
| thm3.8i5 1081 |
(Contributed by Roy F. Lon... |
| lem4.6.2e1 1082 |
Equation 4.10 of [MegPav20... |
| lem4.6.2e2 1083 |
Equation 4.10 of [MegPav20... |
| lem4.6.3le1 1084 |
Equation 4.11 of [MegPav20... |
| lem4.6.3le2 1085 |
Equation 4.11 of [MegPav20... |
| lem4.6.4 1086 |
Equation 4.12 of [MegPav20... |
| lem4.6.5 1087 |
Equation 4.13 of [MegPav20... |
| lem4.6.6i0j1 1088 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i0j2 1089 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i0j3 1090 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i0j4 1091 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i1j0 1092 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i1j2 1093 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i1j3 1094 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i2j0 1095 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i2j1 1096 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i2j4 1097 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i3j0 1098 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i3j1 1099 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i4j0 1100 |
Equation 4.14 of [MegPav20... |
| lem4.6.6i4j2 1101 |
Equation 4.14 of [MegPav20... |
| com3iia 1102 |
The dual of ~ com3ii . (C... |
| lem4.6.7 1103 |
Equation 4.15 of [MegPav20... |
| wdcom 1105 |
Any two variables (weakly)... |
| wdwom 1106 |
Prove 2-variable WOML rule... |
| wddi1 1107 |
Prove the weak distributiv... |
| wddi2 1108 |
The weak distributive law ... |
| wddi3 1109 |
The weak distributive law ... |
| wddi4 1110 |
The weak distributive law ... |
| wdid0id5 1111 |
Show that quantum identity... |
| wdid0id1 1112 |
Show a quantum identity th... |
| wdid0id2 1113 |
Show a quantum identity th... |
| wdid0id3 1114 |
Show a quantum identity th... |
| wdid0id4 1115 |
Show a quantum identity th... |
| wdka4o 1116 |
Show WDOL analog of WOM la... |
| wddi-0 1117 |
The weak distributive law ... |
| wddi-1 1118 |
The weak distributive law ... |
| wddi-2 1119 |
The weak distributive law ... |
| wddi-3 1120 |
The weak distributive law ... |
| wddi-4 1121 |
The weak distributive law ... |
| ml 1123 |
Modular law in equational ... |
| mldual 1124 |
Dual of modular law. (Con... |
| ml2i 1125 |
Inference version of modul... |
| mli 1126 |
Inference version of modul... |
| mldual2i 1127 |
Inference version of dual ... |
| mlduali 1128 |
Inference version of dual ... |
| ml3le 1129 |
Form of modular law that s... |
| ml3 1130 |
Form of modular law that s... |
| vneulem1 1131 |
Part of von Neumann's lemm... |
| vneulem2 1132 |
Part of von Neumann's lemm... |
| vneulem3 1133 |
Part of von Neumann's lemm... |
| vneulem4 1134 |
Part of von Neumann's lemm... |
| vneulem5 1135 |
Part of von Neumann's lemm... |
| vneulem6 1136 |
Part of von Neumann's lemm... |
| vneulem7 1137 |
Part of von Neumann's lemm... |
| vneulem8 1138 |
Part of von Neumann's lemm... |
| vneulem9 1139 |
Part of von Neumann's lemm... |
| vneulem10 1140 |
Part of von Neumann's lemm... |
| vneulem11 1141 |
Part of von Neumann's lemm... |
| vneulem12 1142 |
Part of von Neumann's lemm... |
| vneulem13 1143 |
Part of von Neumann's lemm... |
| vneulem14 1144 |
Part of von Neumann's lemm... |
| vneulem15 1145 |
Part of von Neumann's lemm... |
| vneulem16 1146 |
Part of von Neumann's lemm... |
| vneulem 1147 |
von Neumann's modular law ... |
| vneulemexp 1148 |
Expanded version of ~ vneu... |
| l42modlem1 1149 |
Lemma for ~ l42mod . (Con... |
| l42modlem2 1150 |
Lemma for ~ l42mod . (Con... |
| l42mod 1151 |
An equation that fails in ... |
| modexp 1152 |
Expansion by modular law. ... |
| dp15lema 1154 |
Part of proof (1)=>(5) in ... |
| dp15lemb 1155 |
Part of proof (1)=>(5) in ... |
| dp15lemc 1156 |
Part of proof (1)=>(5) in ... |
| dp15lemd 1157 |
Part of proof (1)=>(5) in ... |
| dp15leme 1158 |
Part of proof (1)=>(5) in ... |
| dp15lemf 1159 |
Part of proof (1)=>(5) in ... |
| dp15lemg 1160 |
Part of proof (1)=>(5) in ... |
| dp15lemh 1161 |
Part of proof (1)=>(5) in ... |
| dp15 1162 |
Part of theorem from Alan ... |
| dp53lema 1163 |
Part of proof (5)=>(3) in ... |
| dp53lemb 1164 |
Part of proof (5)=>(3) in ... |
| dp53lemc 1165 |
Part of proof (5)=>(3) in ... |
| dp53lemd 1166 |
Part of proof (5)=>(3) in ... |
| dp53leme 1167 |
Part of proof (5)=>(3) in ... |
| dp53lemf 1168 |
Part of proof (5)=>(3) in ... |
| dp53lemg 1169 |
Part of proof (5)=>(3) in ... |
| dp53 1170 |
Part of theorem from Alan ... |
| dp35lemg 1171 |
Part of proof (3)=>(5) in ... |
| dp35lemf 1172 |
Part of proof (3)=>(5) in ... |
| dp35leme 1173 |
Part of proof (3)=>(5) in ... |
| dp35lemd 1174 |
Part of proof (3)=>(5) in ... |
| dp35lemc 1175 |
Part of proof (3)=>(5) in ... |
| dp35lemb 1176 |
Part of proof (3)=>(5) in ... |
| dp35lembb 1177 |
Part of proof (3)=>(5) in ... |
| dp35lema 1178 |
Part of proof (3)=>(5) in ... |
| dp35lem0 1179 |
Part of proof (3)=>(5) in ... |
| dp35 1180 |
Part of theorem from Alan ... |
| dp34 1181 |
Part of theorem from Alan ... |
| dp41lema 1182 |
Part of proof (4)=>(1) in ... |
| dp41lemb 1183 |
Part of proof (4)=>(1) in ... |
| dp41lemc0 1184 |
Part of proof (4)=>(1) in ... |
| dp41lemc 1185 |
Part of proof (4)=>(1) in ... |
| dp41lemd 1186 |
Part of proof (4)=>(1) in ... |
| dp41leme 1187 |
Part of proof (4)=>(1) in ... |
| dp41lemf 1188 |
Part of proof (4)=>(1) in ... |
| dp41lemg 1189 |
Part of proof (4)=>(1) in ... |
| dp41lemh 1190 |
Part of proof (4)=>(1) in ... |
| dp41lemj 1191 |
Part of proof (4)=>(1) in ... |
| dp41lemk 1192 |
Part of proof (4)=>(1) in ... |
| dp41leml 1193 |
Part of proof (4)=>(1) in ... |
| dp41lemm 1194 |
Part of proof (4)=>(1) in ... |
| dp41 1195 |
Part of theorem from Alan ... |
| dp32 1196 |
Part of theorem from Alan ... |
| dp23 1197 |
Part of theorem from Alan ... |
| xdp41 1198 |
Part of proof (4)=>(1) in ... |
| xdp15 1199 |
Part of proof (1)=>(5) in ... |
| xdp53 1200 |
Part of proof (5)=>(3) in ... |
| xxdp41 1201 |
Part of proof (4)=>(1) in ... |
| xxdp15 1202 |
Part of proof (1)=>(5) in ... |
| xxdp53 1203 |
Part of proof (5)=>(3) in ... |
| xdp45lem 1204 |
Part of proof (4)=>(5) in ... |
| xdp43lem 1205 |
Part of proof (4)=>(3) in ... |
| xdp45 1206 |
Part of proof (4)=>(5) in ... |
| xdp43 1207 |
Part of proof (4)=>(3) in ... |
| 3dp43 1208 |
"3OA" version of ~ xdp43 .... |
| oadp35lemg 1209 |
Part of proof (3)=>(5) in ... |
| oadp35lemf 1210 |
Part of proof (3)=>(5) in ... |
| oadp35lemc 1211 |
Part of proof (3)=>(5) in ... |
| oadp35 1212 |
Part of theorem from Alan ... |
| testmod 1213 |
A modular law experiment. ... |
| testmod1 1214 |
A modular law experiment. ... |
| testmod2 1215 |
A modular law experiment. ... |
| testmod2expanded 1216 |
A modular law experiment. ... |
| testmod3 1217 |
A modular law experiment. ... |
