-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathw1.txt
59 lines (48 loc) · 2.7 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
% 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 (898 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCNpCCqrpCrp,CCCCpCCNpqrstCst,CCCpqrCqr,CpCCNqCCNrsqCrq,CCCCNNpCpNpqrCpr,CCNpCqpCrCCNsCpsCqs,CCCCNpCqpprCqr
% Concrete (2288 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] CCNpCCqrpCrp = D[2]1
[4] CCCCNpCqpCrpsCCrCCNrtqs = D[3][0]
[5] CCCCpCCNpqrstCst = D[3][1]
[6] CCCpqrCqr = D[3][2]
[7] CCCNCpCCNpqrstCuCCNvCtvCCpCCNpqrv = D[5]1
[8] CCCNpqrCsCCNtCrtCpt = D[6]1
[9] CpCCNqCrqCCNrCCCNsCCCNtCutCvtsCCvCCNvwusrq = D1DD[7][0]1
[10] CpCCqrCNpr = DDD[8]11[2]
[11] CpCCNqCrqCrq = D1D[6][4]
[12] CpCCNqCCNrsqCrq = D1[10]
[13] CpCqCCNrCprCCsCCNstur = D[5][7]
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 33 steps
[14] CpCqp = D[6][5]
[15] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[3][9]
[16] CCpqCpq = D[3][11]
[17] CCCNpqrCpr = D[3][12]
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 87 steps
[18] CpCNpq = D[17][16]
[19] CCCCNNpCpNpqrCpr = D[3]D1D[5]D[5]D[4]D[4][6]
[20] CCNpCqpCrCCNsCpsCqs = DD[3]D[8]DD[9]1[9][8]
[21] CpCCpNpq = D[19][6]
[22] CCCCNpCqpCrpsCCrqs = D[3]D1D[6][20]
% Identity principle (Cpp), i.e. 0→0 ; 143 steps
[23] Cpp = DD[12]1[21]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 151 steps
[24] CCpqCCqrCpr = D[6]DD[3]D1[20][6]
[25] CCCCNpCqpprCqr = D[3]D1DD[3]D1[13]D[4]D[3]D[13]D[19]D[3]D[8][14]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 323 steps
[26] CCNppp = D[3]D[25][16]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 341 steps
[27] CCNpNqCqp = DDD1D[22]D[3]DD[6][13][21]1[12]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1071 steps
[28] CCpCqrCCpqCpr = DDD[8]D[15]D[22]D[3]D1D[25]D[6]D[5]D[6]D[4]D[3]D[13][2]1DD[3]D1DDD[0]1DD[3]D[8]D[3]D1D[6]D[6]DDD[8]D[3]D[8]DD[11]1D[17][15]1[0]D[6][10]1D[5]D[5]DD[3]D1DD[3]D[7]DD[3]D1D[15]1[6]1[6]