forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathw1.txt
65 lines (54 loc) · 3 KB
/
w1.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
% Walsh's 1st Axiom (CCpCCNpqrCsCCNtCrtCpt), i.e. (0→((¬0→1)→2))→(3→((¬4→(2→4))→(0→4)))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CCpCCNpqrCsCCNtCrtCpt
% SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c
%
% Full summary: pmGenerator --transform data/w1.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w1.txt -f -n -t . -p -2 -d
% pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (1068 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCNpCCqrpCrp,CCCCpCCNpqrstCst,CCCpqrCqr,CpCCNqCrqCrq,CpCCNqCCNrsqCrq,CCCCNNpCpNpqrCpr,CCNpCqpCrCCNsCpsCqs,CCCCpqCrqsCCrps,CCCCNpCqpprCqr
% Concrete (3144 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
CCpCCNpqrCsCCNtCrtCpt = 1
[0] CpCCNqCCCNrCsrCtrqCCtCCNtusq = D11
[1] CpCCNqCCCrCCNrstuqCuq = D1[0]
[2] CpCCNqCCrsqCsq = D1[1]
[3] CCNpCCCqCCNqrstpCtp = D[1]1
[4] CCNpCCqrpCrp = D[2]1
[5] CCCCNpCqpCrpsCCrCCNrtqs = D[4][0]
[6] CCCCpCCNpqrstCst = D[4][1]
[7] CCCpqrCqr = D[4][2]
[8] CCCNCpCCNpqrstCuCCNvCtvCCpCCNpqrv = D[6]1
[9] CCCNpqrCsCCNtCrtCpt = D[7]1
[10] CpCCNqCrqCCNrCCCNsCCCNtCutCvtsCCvCCNvwusrq = D1DD[8][0]1
[11] CpCCNqCrqCCNrCCCNsCCtusCusrq = D1DD[8][2]1
[12] CpCCNqCrqCrq = D1D[7][5]
[13] CpCCNqCCNrsqCrq = D1DDD[9]11[2]
[14] CpCqCCNrCprCCsCCNstur = D[6][8]
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 33 steps
[15] CpCqp = D[7][6]
[16] CCNpCqpCqp = D[12]1
[17] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[4][10]
[18] CpCqCCNrCprCsr = D[6][9]
[19] CCpqCpq = D[4][12]
[20] CCCNpqrCpr = D[4][13]
[21] CpCqCCNrCsrCNpr = D[20]1
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 87 steps
[22] CpCNpq = D[20][19]
[23] CCCCNNpCpNpqrCpr = D[4]D1D[6]D[6]D[5]D[5][7]
[24] CCNpCqpCrCCNsCpsCqs = DD[4]D[9]DD[10]1[10][9]
[25] CpCCpNpq = D[23][7]
% Identity principle (Cpp), i.e. 0→0 ; 143 steps
[26] Cpp = DD[13]1[25]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 151 steps
[27] CCpqCCqrCpr = D[7]DD[4]D1[24][7]
[28] CNpCpq = D[23]D[4]D[9][15]
[29] CCCCpqCrqsCCrps = D[4]D[9]DD[4][11][27]
[30] CCCCNpCqpCCrCCNrstpuCqu = D[4]D1[14]
[31] CCCCNpCqpprCqr = D[4]D1D[30]D[5]D[4]D[14][28]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 323 steps
[32] CCNppp = D[4]D[31][19]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 343 steps
[33] CCNpNqCqp = DDD1DD[4]D1D[7][24]D[4]DD[7][18][25]1[13]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1925 steps
[34] CCpCqrCCpqCpr = DD[29]D[4]D1D[30]DD[4]D[9]D[17][7]D[5]D[4]D[18][28]D[29]DD[16]DD[4]D[3]DD[4]D1DDD[18]D[6]D[7]D[5][22]1[11]D[7]D[7][21]D[31][7]DD[4]D[3]DD[4]D[9]D[4]D1DD[4]D1[18]DDD[9]D[4]D[9]D[16]D[20][17]1[0][21]D[6]D[6]DD[4]D1DD[4]D[8]DD[4]D1D[17]1[7]1[7]