mmplot/proof_with_comments.txt at master · void4/mmplot · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
dummylink;inference
idi;inference
mp2;inference
mp2b;inference
a1i;axiom
mp1i;antecedent
a2i;axiom
imim2i;inference
mpd;see
syl;inference
mpi;inference
mp2ALT;wolf
3syl;inference
4syl;inference
id;see
id1;see
idd;identity
a1d;axiom
a2d;antecedent
a1ii;axiom
a1iiALT;axiom
sylcom;inference
syl5com;inference
com12;inference
syl5;inference
syl6;inference
syl56;combine
syl6com;inference
mpcom;inference
syli;inference
syl2im;wolf
pm2.27;closed
mpdd;modus
mpid;modus
mpdi;modus
mpii;inference
syld;form
mp2d;wolf
a1dd;antecedent
pm2.43i;inference
pm2.43d;antecedent
pm2.43a;inference
pm2.43b;inference
pm2.43;axiom
imim2d;adding
imim2;closed
embantd;wolf
3syld;hankins,
sylsyld;alan
imim12i;inference
imim1i;inference
imim3i;inference
sylc;inference
syl3c;inference
syl6mpi;alan
mpsyl;inference
syl6c;inference
syldd;wolf
syl5d;syllogism
syl7;inference
syl6d;syllogism
syl8;inference
syl9;inference
syl9r;inference
imim12d;antecedents
imim1d;wolf
imim1;closed
pm2.83;[whiteheadrussell]
com23;wolf
com3r;right
com13;wolf
com3l;wolf
pm2.04;wolf
com34;antecedents
com4l;left
com4t;antecedents
com4r;right
com24;wolf
com14;wolf
com45;hankins,
com35;hankins,
com25;hankins,
com5l;wolf
com15;wolf
com52l;hankins,
com52r;hankins,
com5r;wolf
jarr;inference
pm2.86i;inference
pm2.86d;wolf
pm2.86;axiom
loolin;axiom
loowoz;axiom
con4d;axiom
pm2.21d;implies
pm2.21dd;implies
pm2.21;wolf
pm2.24;[whiteheadrussell]
pm2.18;also
pm2.18d;fl,
notnot2;when
notnotrd;definition
notnotri;inference
con2d;contraposition
con2;wolf
mt2d;modus
mt2i;inference
nsyl3;inference
con2i;inference
nsyl;inference
notnot1;wolf
notnoti;double
con1d;contraposition
mt3d;modus
mt3i;inference
nsyl2;inference
con1;wolf
con1i;inference
con4i;axiom
pm2.21i;inference
pm2.24ii;inference
con3d;contraposition
con3;wolf
con3i;inference
con3rr3;wolf
mt4;wolf
mt4d;modus
mt4i;inference
nsyld;syllogism
nsyli;inference
nsyl4;inference
pm2.24d;None
pm2.24i;inference
pm3.2im;[whiteheadrussell]
mth8;[margaris]
jc;inference
impi;inference
expi;inference
simprim;wolf
simplim;wolf
pm2.5;wolf
pm2.51;[whiteheadrussell]
pm2.521;wolf
pm2.52;wolf
expt;expressed
impt;wolf
pm2.61d;wolf
pm2.61d1;inference
pm2.61d2;inference
ja;inference
jad;form
jarl;inference
pm2.61i;inference
pm2.61ii;inference
pm2.61nii;inference
pm2.61iii;inference
pm2.01;wolf
pm2.01d;wolf
pm2.6;[whiteheadrussell]
pm2.61;wolf
pm2.65;wolf
pm2.65i;inference
pm2.65d;wolf
mto;wolf
mtod;wolf
mtoi;inference
mt2;wolf
mt3;wolf
peirce;axiom
looinv;axiom
bijust;definition
bi1;property
bi3;property
impbii;equivalence
impbidd;equivalence
impbid21d;wolf
impbid;wolf
dfbi1;see
dfbi1gb;property
biimpi;equivalence
sylbi;definition
sylib;inference
bi2;property
bicom1;wolf
bicom;equivalence
bicomd;sides
bicomi;inference
impbid1;equivalence
impbid2;wolf
impcon4bid;hankins,
biimpri;wolf
biimpd;equivalence
mpbi;inference
mpbir;inference
mpbid;modus
mpbii;inference
sylibr;definition
sylbir;inference
sylibd;syllogism
sylbid;syllogism
mpbidi;modus
syl5bi;definition
syl5bir;inference
syl5ib;inference
syl5ibcom;inference
syl5ibr;inference
syl5ibrcom;inference
biimprd;wolf
biimpcd;wolf
biimprcd;wolf
syl6ib;inference
syl6ibr;definition
syl6bi;inference
syl6bir;inference
syl7bi;inference
syl8ib;inference
mpbird;modus
mpbiri;inference
sylibrd;syllogism
sylbird;syllogism
biid;identity
biidd;identity
pm5.1im;closed
2th;equivalent
2thd;rule
ibi;inference
ibir;inference
ibd;into
pm5.74;over
pm5.74i;inference
pm5.74ri;inference
pm5.74d;over
pm5.74rd;over
bitri;inference
bitr2i;inference
bitr3i;inference
bitr4i;inference
bitrd;form
bitr2d;form
bitr3d;form
bitr4d;form
syl5bb;inference
syl5rbb;inference
syl5bbr;inference
syl5rbbr;inference
syl6bb;inference
syl6rbb;inference
syl6bbr;inference
syl6rbbr;inference
3imtr3i;definition
3imtr4i;definition
3imtr3d;more
3imtr4d;more
3imtr3g;wolf
3imtr4g;wolf
3bitri;inference
3bitrri;inference
3bitr2i;inference
3bitr2ri;inference
3bitr3i;inference
3bitr3ri;inference
3bitr4i;definition
3bitr4ri;inference
3bitrd;biconditional
3bitrrd;biconditional
3bitr2d;biconditional
3bitr2rd;biconditional
3bitr3d;biconditional
3bitr3rd;biconditional
3bitr4d;biconditional
3bitr4rd;biconditional
3bitr3g;more
3bitr4g;more
bi3ant;wolf
bisym;terms
notnot;[whiteheadrussell]
con34b;[whiteheadrussell]
con4bid;contraposition
notbid;equivalence
notbi;wolf
notbii;wolf
con4bii;inference
mtbi;inference
mtbir;inference
mtbid;similar
mtbird;similar
mtbii;inference
mtbiri;inference
sylnib;inference
sylnibr;definition
sylnbi;definition
sylnbir;inference
xchnxbi;wolf
xchnxbir;wolf
xchbinx;wolf
xchbinxr;wolf
imbi2i;wolf
bibi2i;inference
bibi1i;inference
bibi12i;equivalence
imbi2d;equivalence
imbi1d;wolf
bibi2d;wolf
bibi1d;equivalence
imbi12d;form
bibi12d;form
imbi1;[whiteheadrussell]
imbi2;wolf
imbi1i;wolf
imbi12i;form
bibi1;[whiteheadrussell]
con2bi;wolf
con2bid;contraposition
con1bid;contraposition
con1bii;inference
con2bii;inference
con1b;contraposition
con2b;contraposition
biimt;antecedent
pm5.5;[whiteheadrussell]
a1bi;inference
mt2bi;wolf
mtt;wolf
pm5.501;[whiteheadrussell]
ibib;terms
ibibr;terms
tbt;equivalence
nbn2;wolf
bibif;wolf
nbn;wolf
nbn3;equivalence
pm5.21im;closed
2false;wolf
2falsed;rule
pm5.21ni;wolf
pm5.21nii;antecedent
pm5.21ndd;wolf
bija;see
pm5.18;same
xor3;express
nbbn;wolf
biass;axiom
pm5.19;[whiteheadrussell]
bi2.04;equivalence
pm5.4;antecedent
imdi;[whiteheadrussell]
pm5.41;wolf
pm4.8;[whiteheadrussell]
pm4.81;[whiteheadrussell]
imim21b;form
pm4.64;[whiteheadrussell]
pm2.53;[whiteheadrussell]
pm2.54;[whiteheadrussell]
ori;implication
orri;implication
ord;implication
orrd;implication
jaoi;inference
jaod;antecedents
mpjaod;eliminate
orel1;wolf
orel2;wolf
olc;axiom
orc;[whiteheadrussell]
pm1.4;axiom
orcom;wolf
orcomd;commutation
orcoms;antecedent
orci;wolf
olci;wolf
orcd;\/
olcd;\/
orcs;inference
olcs;wolf
pm2.07;[whiteheadrussell]
pm2.45;[whiteheadrussell]
pm2.46;[whiteheadrussell]
pm2.47;[whiteheadrussell]
pm2.48;[whiteheadrussell]
pm2.49;[whiteheadrussell]
pm2.67-2;[whiteheadrussell]
pm2.67;[whiteheadrussell]
pm2.25;[whiteheadrussell]
biorf;wolf
biortn;equivalent
biorfi;equivalent
pm2.621;[whiteheadrussell]
pm2.62;wolf
pm2.68;[whiteheadrussell]
dfor2;terms
imor;terms
imori;implication
imorri;jonathan
exmid;no
exmidd;middle
pm2.1;wolf
pm2.13;[whiteheadrussell]
pm4.62;[whiteheadrussell]
pm4.66;[whiteheadrussell]
pm4.63;[whiteheadrussell]
imnan;terms
imnani;terms
iman;terms
annim;terms
pm4.61;[whiteheadrussell]
pm4.65;[whiteheadrussell]
pm4.67;[whiteheadrussell]
imp;inference
impcom;inference
imp3a;importation
imp31;inference
imp32;inference
ex;inference
expcom;inference
exp3a;exportation
expdimp;importation
impancom;inference
con3and;jonathan
pm2.01da;based
pm2.18da;based
pm3.3;wolf
pm3.31;wolf
impexp;wolf
pm3.2;wolf
pm3.21;conjunction
pm3.22;wolf
ancom;wolf
ancomd;hankins,
ancoms;inference
ancomsd;antecedent
pm3.2i;conjunction
pm3.43i;conjunction
simpl;wolf
simpli;inference
simpld;see
simplbi;conjunct
simpr;wolf
simpri;inference
simprd;see
simprbi;conjunct
adantr;inference
adantl;inference
adantld;wolf
adantrd;antecedent
mpan9;antecedents
syldan;wolf
sylan;inference
sylanb;inference
sylanbr;inference
sylan2;inference
sylan2b;inference
sylan2br;inference
syl2an;inference
syl2anr;inference
syl2anb;inference
syl2anbr;inference
syland;syllogism
sylan2d;syllogism
syl2and;syllogism
biimpa;inference
biimpar;inference
biimpac;inference
biimparc;inference
ianor;terms
anor;terms
ioran;terms
pm4.52;wolf
pm4.53;[whiteheadrussell]
pm4.54;wolf
pm4.55;[whiteheadrussell]
pm4.56;[whiteheadrussell]
oran;terms
pm4.57;[whiteheadrussell]
pm3.1;[whiteheadrussell]
pm3.11;[whiteheadrussell]
pm3.12;[whiteheadrussell]
pm3.13;[whiteheadrussell]
pm3.14;[whiteheadrussell]
iba;antecedent
ibar;antecedent
biantru;conjunction
biantrur;conjunction
biantrud;wolf
biantrurd;conjunction
jaao;inference
jaoa;inference
pm3.44;wolf
jao;wolf
pm1.2;axiom
oridm;wolf
pm4.25;[whiteheadrussell]
orim12i;wolf
orim1i;both
orim2i;both
orbi2i;inference
orbi1i;inference
orbi12i;disjunction
pm1.5;axiom
or12;wolf
orass;[whiteheadrussell]
pm2.31;[whiteheadrussell]
pm2.32;[whiteheadrussell]
or32;rearrangement
or4;4
or42;4
orordi;over
orordir;over
jca;see
jcad;wolf
jca31;hankins,
jca32;fl,
jcai;conjunction
jctil;inference
jctir;inference
jctl;inference
jctr;inference
jctild;left
jctird;implication
ancl;left
anclb;wolf
pm5.42;[whiteheadrussell]
ancr;antecedent
ancrb;wolf
ancli;left
ancri;antecedent
ancld;wolf
ancrd;wolf
anc2l;wolf
anc2r;antecedent
anc2li;wolf
anc2ri;wolf
pm3.41;[whiteheadrussell]
pm3.42;[whiteheadrussell]
pm3.4;conjunction
pm4.45im;conjunction
anim12d;wolf
anim1d;antecedent
anim2d;left
anim12i;wolf
anim12ci;jonathan
anim1i;both
anim2i;both
anim12ii;wolf
prth;closed
pm2.3;[whiteheadrussell]
pm2.41;[whiteheadrussell]
pm2.42;[whiteheadrussell]
pm2.4;[whiteheadrussell]
pm2.65da;rule
pm4.44;[whiteheadrussell]
pm4.14;wolf
pm3.37;wolf
nan;out
pm4.15;wolf
pm4.78;over
pm4.79;wolf
pm4.87;[whiteheadrussell]
pm3.33;[whiteheadrussell]
pm3.34;[whiteheadrussell]
pm3.35;[whiteheadrussell]
pm5.31;[whiteheadrussell]
imp4a;inference
imp4b;inference
imp4c;inference
imp4d;inference
imp41;inference
imp42;inference
imp43;inference
imp44;inference
imp45;inference
imp5a;inference
imp5d;inference
imp5g;inference
imp55;inference
imp511;inference
expimpd;importation
exp31;inference
exp32;inference
exp4a;inference
exp4b;inference
exp4c;inference
exp4d;inference
exp41;inference
exp42;inference
exp43;inference
exp44;inference
exp45;inference
expr;hankins,
exp5c;inference
exp53;inference
expl;hankins,
impr;into
impl;left
impac;conjunction
exbiri;inference
simprbda;conjunct
simplbda;conjunct
simplbi2;alan
dfbi2;definition
dfbi;definition
pm4.71;terms
pm4.71r;terms
pm4.71i;inference
pm4.71ri;inference
pm4.71d;conjunction
pm4.71rd;conjunction
pm5.32;over
pm5.32i;inference
pm5.32ri;inference
pm5.32d;over
pm5.32rd;over
pm5.32da;over
biadan2;madsen,
pm4.24;[whiteheadrussell]
anidm;wolf
anidms;inference
anidmdbi;antecedent
anasss;antecedent
anassrs;antecedent
anass;wolf
sylanl1;inference
sylanl2;inference
sylanr1;inference
sylanr2;inference
sylani;inference
sylan2i;inference
syl2ani;inference
sylan9;inference
sylan9r;inference
mtand;hankins,
mtord;hankins,
syl2anc;inference
sylancl;inference
sylancr;inference
sylanbrc;inference
sylancb;inference
sylancbr;inference
sylancom;inference
mpdan;inference
mpancom;inference
mpan;inference
mpan2;inference
mp2an;inference
mp4an;inference
mpan2d;based
mpand;wolf
mpani;inference
mpan2i;inference
mp2ani;inference
mp2and;based
mpanl1;inference
mpanl2;inference
mpanl12;inference
mpanr1;inference
mpanr2;inference
mpanr12;inference
mpanlr1;inference
pm5.74da;over
pm4.45;[whiteheadrussell]
imdistan;wolf
imdistani;conjunction
imdistanri;conjunction
imdistand;rule
imdistanda;madsen,
anbi2i;wolf
anbi1i;wolf
anbi2ci;jonathan
anbi12i;both
anbi12ci;jonathan
sylan9bb;inference
sylan9bbr;inference
orbi2d;equivalence
orbi1d;equivalence
anbi2d;wolf
anbi1d;wolf
orbi1;[whiteheadrussell]
anbi1;equivalence
anbi2;equivalence
bitr;[whiteheadrussell]
orbi12d;form
anbi12d;form
pm5.3;[whiteheadrussell]
pm5.61;wolf
adantll;wolf
adantlr;wolf
adantrl;wolf
adantrr;wolf
adantlll;wolf
adantllr;wolf
adantlrl;wolf
adantlrr;wolf
adantrll;wolf
adantrlr;wolf
adantrrl;wolf
adantrrr;wolf
ad2antrr;wolf
ad2antlr;wolf
ad2antrl;antecedent
ad2antll;antecedent
ad3antrrr;antecedent
ad3antlr;antecedent
ad4antr;antecedent
ad4antlr;antecedent
ad5antr;antecedent
ad5antlr;antecedent
ad6antr;antecedent
ad6antlr;antecedent
ad7antr;antecedent
ad7antlr;antecedent
ad8antr;antecedent
ad8antlr;antecedent
ad9antr;antecedent
ad9antlr;antecedent
ad10antr;antecedent
ad10antlr;antecedent
ad2ant2l;antecedent
ad2ant2r;antecedent
ad2ant2lr;antecedent
ad2ant2rl;antecedent
simpll;conjunction
simplr;conjunction
simprl;conjunction
simprr;conjunction
simplll;hankins,
simpllr;hankins,
simplrl;hankins,
simplrr;hankins,
simprll;hankins,
simprlr;hankins,
simprrl;hankins,
simprrr;hankins,
simp-4l;conjunction
simp-4r;conjunction
simp-5l;conjunction
simp-5r;conjunction
simp-6l;conjunction
simp-6r;conjunction
simp-7l;conjunction
simp-7r;conjunction
simp-8l;conjunction
simp-8r;conjunction
simp-9l;conjunction
simp-9r;conjunction
simp-10l;conjunction
simp-10r;conjunction
simp-11l;conjunction
simp-11r;conjunction
jaob;wolf
jaoian;inference
jaodan;antecedents
mpjaodan;\/
pm4.77;[whiteheadrussell]
pm2.63;[whiteheadrussell]
pm2.64;[whiteheadrussell]
pm2.61ian;antecedent
pm2.61dan;antecedent
pm2.61ddan;elimination
pm2.61dda;elimination
condan;wolf
abai;wolf
pm5.53;[whiteheadrussell]
an12;first
an32;wolf
an13;wolf
an31;wolf
an12s;antecedent
ancom2s;inference
an13s;antecedent
an32s;antecedent
ancom1s;inference
an31s;antecedent
anass1rs;madsen,
anabs1;wolf
anabs5;wolf
anabs7;wolf
anabsan;antecedent
anabss1;wolf
anabss4;into
anabss5;wolf
anabsi5;wolf
anabsi6;into
anabsi7;wolf
anabsi8;into
anabss7;wolf
anabsan2;antecedent
anabss3;wolf
an4;4
an42;4
an4s;inference
an42s;inference
anandi;over
anandir;over
anandis;inference
anandirs;inference
impbida;equivalence
pm3.48;[whiteheadrussell]
pm3.45;[whiteheadrussell]
im2anan9;form
im2anan9r;form
anim12dan;antecedents
orim12d;antecedents
orim1d;antecedents
orim2d;antecedents
orim2;sum
pm2.38;[whiteheadrussell]
pm2.36;[whiteheadrussell]
pm2.37;[whiteheadrussell]
pm2.73;[whiteheadrussell]
pm2.74;[whiteheadrussell]
orimdi;over
pm2.76;[whiteheadrussell]
pm2.75;wolf
pm2.8;wolf
pm2.81;[whiteheadrussell]
pm2.82;[whiteheadrussell]
pm2.85;wolf
pm3.2ni;disjunction
orabs;wolf
oranabs;wolf
pm5.1;both
pm5.21;both
pm3.43;[whiteheadrussell]
jcab;over
ordi;wolf
ordir;distributive
pm4.76;[whiteheadrussell]
andi;wolf
andir;conjunction
orddi;double
anddi;conjunction
pm4.39;[whiteheadrussell]
pm4.38;[whiteheadrussell]
bi2anan9;form
bi2anan9r;form
bi2bian9;different
pm4.72;terms
imimorb;between
pm5.33;[whiteheadrussell]
pm5.36;[whiteheadrussell]
bianabs;into
oibabs;wolf
pm3.24;wolf
pm2.26;wolf
pm5.11;[whiteheadrussell]
pm5.12;[whiteheadrussell]
pm5.14;[whiteheadrussell]
pm5.13;wolf
pm5.17;wolf
pm5.15;wolf
pm5.16;wolf
xor;wolf
nbi2;wolf
dfbi3;definition
pm5.24;[whiteheadrussell]
xordi;multiplication
biort;true
pm5.55;wolf
pm5.21nd;wolf
pm5.35;[whiteheadrussell]
pm5.54;wolf
baib;conjunction
baibr;conjunction
rbaib;conjunction
rbaibr;conjunction
baibd;conjunction
rbaibd;conjunction
pm5.44;[whiteheadrussell]
pm5.6;antecedent
orcanai;antecedent
intnan;conjunct
intnanr;conjunct
intnand;conjunct
intnanrd;conjunct
mpbiran;conjunction
mpbiran2;conjunction
mpbir2an;conjunction
mpbi2and;wolf
mpbir2and;wolf
pm5.62;[whiteheadrussell]
pm5.63;wolf
bianfi;wolf
bianfd;wolf
pm4.43;wolf
pm4.82;[whiteheadrussell]
pm4.83;[whiteheadrussell]
pclem6;wolf
biantr;equivalence
orbidi;axiom
biluk;axiom
pm5.7;over
bigolden;rule
pm5.71;[whiteheadrussell]
pm5.75;wolf
bimsc1;equivalence
4exmid;david
ecase2d;wolf
ecase3;inference
ecase;inference
ecase3d;elimination
ecased;elimination
ecase3ad;elimination
ccase;inference
ccased;cases
ccase2;inference
4cases;inference
4casesdan;their
niabn;inference
dedlem0a;wolf
dedlem0b;alternate
dedlema;weak
dedlemb;weak
elimh;see
dedt;see
con3th;use
consensus;\/
pm4.42;[whiteheadrussell]
ninba;inference
prlem1;axiom
prlem2;axiom
oplem1;pair
rnlem;numbers
dn1;axiom
jaoi2;inference
jaoi2OLD;obsolete
jaoi3;inference
3orass;triple
3anass;conjunction
3anrot;conjunction
3orrot;triple
3ancoma;conjunction
3orcoma;triple
3ancomb;conjunction
3orcomb;triple
3anrev;conjunction
3anan32;jonathan
3anan12;jonathan
anandi3;over
anandi3r;over
3anor;terms
3ianor;terms
3ioran;conjunction
3oran;terms
3simpa;conjunction
3simpb;conjunction
3simpc;conjunction
simp1;conjunction
simp2;conjunction
simp3;conjunction
simpl1;rule
simpl2;rule
simpl3;rule
simpr1;rule
simpr2;rule
simpr3;rule
simp1i;conjunction
simp2i;conjunction
simp3i;conjunction
simp1d;conjunction
simp2d;conjunction
simp3d;conjunction
simp1bi;jonathan
simp2bi;jonathan
simp3bi;jonathan
3adant1;antecedent
3adant2;antecedent
3adant3;antecedent
3ad2ant1;antecedent
3ad2ant2;antecedent
3ad2ant3;antecedent
simp1l;conjunction
simp1r;conjunction
simp2l;conjunction
simp2r;conjunction
simp3l;conjunction
simp3r;conjunction
simp11;conjunction
simp12;conjunction
simp13;conjunction
simp21;conjunction
simp22;conjunction
simp23;conjunction
simp31;conjunction
simp32;conjunction
simp33;conjunction
simpll1;conjunction
simpll2;conjunction
simpll3;conjunction
simplr1;conjunction
simplr2;conjunction
simplr3;conjunction
simprl1;conjunction
simprl2;conjunction
simprl3;conjunction
simprr1;conjunction
simprr2;conjunction
simprr3;conjunction
simpl1l;conjunction
simpl1r;conjunction
simpl2l;conjunction
simpl2r;conjunction