-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
w2.txt
79 lines (66 loc) · 4.57 KB
/
w2.txt
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
% Walsh's 2nd Axiom (CpCCqCprCCNrCCNstqCsr), i.e. 0→((1→(0→2))→((¬2→((¬3→4)→1))→(3→2)))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr
% SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff
%
% Full summary: pmGenerator --transform data/w2.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w2.txt -f -n -t . -p -2 -d
% pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (1620 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps,CCpCCqCrCsCtquCCNuCCNvwpCvu,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CpCCNqCCNCrCNpstNCuCCvCuwCCNwCCNxyvCxwq,CpCCNqCCNrsCpqCrq,CCpCCqCCNrCCNCsCNqtuNCvCwCCxCwyCCNyCCNzaxCzyrbCCNbCCNcdpCcb,CNCpCqNrCsCtCur,CCNCCpqCrqCCNstCNqCCNrupCsCCpqCrq,CCNCCpqqpCCpqq,CCpCqCprCqCpr,CCpqCCNppq,CCpCqrCCqpCqr,CCpCqrCpCqCsr
% Concrete (40960 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqpCCNwxCsCvpCwCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqp = D[0]1
[2] CCNCpqCCNrsCCCNtCCNuvNpCutCCwCCxCwyCCNyCCNzaxCzyqCrCpq = D[0][0]
[3] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
[4] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = D[1]1
[5] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[4]1
[6] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[5]1
[7] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[6]
[8] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[7][0]
[9] CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq = D[1][6]
[10] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[3][6]
[11] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][10]
[12] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1D[8]11
% Identity principle (Cpp), i.e. 0→0 ; 35 steps
[13] Cpp = DD[0]D[2][6][6]
[14] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = D[11][6]
[15] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNybrCzCpCyx = DDD1[10]1[6]
[16] CNpCCNqCCNrspCrq = D[12][6]
[17] CCpCCqqrCCNrCCNstpCsr = D1[13]
[18] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = D[17]1
[19] CpCqCrCsCtq = DDDDD1DD[0][3][6]1[6]11
[20] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[19]1
[21] CCNCpCNqrCCNstqCsCpCNqr = D[0]D[2]DD[15]11
[22] CCCNpqrCCNCpsCCNtuNrCtCps = DDD1[16]1[6]
[23] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[8]DD[0]DDD1DDD1[3]111[6]1
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
[24] CpCqp = DD[20][0]1
[25] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[10][14]
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
[26] CpCNpq = D[25]1
[27] CpCCNqCCNCrCNpstNCuCCvCuwCCNwCCNxyvCxwq = D[25]DDD[0][7][6][5]
[28] CpCCNqCCNrsCpqCrq = DD[0][18][23]
[29] CCpCCqCCNrCCNCsCNqtuNCvCwCCxCwyCCNyCCNzaxCzyrbCCNbCCNcdpCcb = D1D[25]DD[0]DD[7]DDD1[4]1[6]11
[30] CNCpCqNrCsCtCur = DDD1DD[0]DD[9][12][6]1DDD1[20]1[6][6]
[31] CCNCCpqqCCNrspCrCCpqq = D[29][28]
[32] CCNCpCqrCCNstCNrCCNquCprCsCpCqr = D[29]DDD1[28]1[27]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 367 steps
[33] CCNppp = DDD[18]DDD[0]D[2]DDD1[19]DDD1[11]111[30]11[27]
[34] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = D[29]DDD1[33]1[27]
[35] CCNCCpqCrqCCNstCNqCCNrupCsCCpqCrq = D[29]DDD1DDD1D[31][27]1[27]1[27]
[36] CCCNpqrCCrsCps = D[35][6]
[37] CpCCNCpqCpqq = D[34][27]
[38] CCNpCCNqrsCCspCqp = D[35][27]
[39] CCNCCpqqpCCpqq = D[31][37]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1007 steps
[40] CCNpNqCqp = DD[29]DDD1DDD1[37][13]11[27][27]
[41] CCpCqCprCqCpr = D[39]DDD[0]D[21][6]DD[0]DDD1[22]1[6][6]1
[42] CCpqCCNppq = D[38]D[34]DDD[0]DD[0][21][6][30]1
[43] CCpCqrCCqpCqr = D[38]D[34]D[24]DD[39]DDD1DD[0][9][6]D[22][14][23]D[31]D[24]DDD[29][17][27]D[39]DD[8]DDD[0][15][6]D[20][16]1
[44] CCpCqrCpCqCsr = D[43]DD[0]DD[9]D[32][27][6][6]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 11703 steps
[45] CCpqCCqrCpr = D[41]D[44]DD[36]D[42]D[32][23][43]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 27599 steps
[46] CCpCqrCCpqCpr = DD[45]D[41]D[44]DD[36]D[42]D[35][23][43][43]