forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathw5.txt
44 lines (35 loc) · 2.36 KB
/
w5.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
% Walsh's 5th Axiom (CCpqCCCrCstCqCNsNpCps), i.e. (0→1)→(((2→(3→4))→(1→(¬3→¬0)))→(0→3))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CCpqCCCrCstCqCNsNpCps
% SHA-512/224 hash: 1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72
%
% Full summary: pmGenerator --transform data/w5.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w5.txt -f -n -t . -p -2 -d
% pmGenerator --transform data/w5.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (564 bytes): pmGenerator --transform data/w5.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCqrCCCsqtCNqNsCsq
% Concrete (708 bytes): pmGenerator --transform data/w5.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
CCpqCCCrCstCqCNsNpCps = 1
[0] CCCpCqrCCCCsCtuCvCNtNwCwtCNqNCwvCCwvq = D11
[1] CCCpCqrCCCstuCNqNCCvCuwCCCCxCyzCtCNyNsCsyCNuNCstCCCvCuwCCCCxCyzCtCNyNsCsyCNuNCstq = D1[0]
[2] CCpqCCCrCstCCpuCNsNCCvCuwCqCNuNpCCCvCuwCqCNuNps = D[0][0]
[3] CCCCCpCqrCsCNqNtCtquCCtsu = D[0][1]
[4] CCCpCqrCCCstuCNqNCCvCuwCCCCxCyzCCsaCNyNCCbCacCtCNaNsCCCbCacCtCNaNsyCNuNCstCCCvCuwCCCCxCyzCCsaCNyNCCbCacCtCNaNsCCCbCacCtCNaNsyCNuNCstq = D1D1[2]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 15 steps
[5] CCpqCCqrCpr = D[0]D1[3]
[6] CCCpCqrCCCstCutCNqNCusCCusq = D1[5]
[7] CCCCCpCqrCsCNqNtCtqCCuCNCtsvCCwxCNNCtsNNwCCtsw = D[0]D1D[0]D1D[4][1]
[8] CCCpCqrCCCstCCuvCwvCNqNCwuCCwuq = D1D[0]DD1D1DD1D1[1][1]D1D[1][1]
[9] CCCpCqrCCCsqtCNqNsCsq = DD[0]D[1]D1D[1][7]1
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 51 steps
[10] CpCNpq = D[9]1
% Identity principle (Cpp), i.e. 0→0 ; 65 steps
[11] Cpp = D[9][5]
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 83 steps
[12] CpCqp = DD[0]DD[0]D[2]D1DD[0]D[0]D1D[0]D1D[4][7]1[0]1
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 95 steps
[13] CCNpNqCqp = D[8]D1D1[10]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 103 steps
[14] CCNppp = D[6]D[0]D1D[0]D1DD1D[0]D1D1D[0]D1D[0]D1DD1[8][0][1]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 157 steps
[15] CCpCqrCCpqCpr = D[3]DD1D[0]D1DD[0]D1[9]D[0]D1DD1D1D[0]D1D[0]D1D[1][0][1]D1D[0]D1D1D[0]D1D[0]D1D[1][6]