w2:L2:781↦535

- solution from #2 (comment) (discussions)
- manual revision of previous proof with https://github.com/metamath/metamath-exe
- based on e4602a2

Co-authored-by: Gino Giotto <73717712+GinoGiotto@users.noreply.github.com>

data/w2.txt

@@ -7,39 +7,33 @@
 % 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,Cpp,CpCNpq,CCNppp -p -2 -d
-% Compact (638 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp
-% Concrete (1008 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -e
+% Compact (498 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq
+% Concrete (762 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -e
 
     CpCCqCprCCNrCCNstqCsr = 1
 [0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
-[1] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
-[2] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[1]1
-[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[2]1
-[4] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
+[1] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
+[2] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
+[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DD[2]11
+[4] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[3]
+[5] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
+[6] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[1][3]
+[7] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][6]
 
 % Identity principle (Cpp), i.e. 0→0 ; 35 steps
-[5] Cpp = DD[0][4][3]
+[8] Cpp = DD[0][5][3]
 
-[6] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
-[7] CpCqCrCsCtq = DDDDD1DD[0][6][3]1[3]11
-[8] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[7]1
+[9] CCpCCqqrCCNrCCNstpCsr = D1[8]
+[10] CpCqCrCsCtq = DDDDD1DD[0][1][3]1[3]11
+[11] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[10]1
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
-[9] CpCqp = DD[8][0]1
+[12] CpCqp = DD[11][0]1
 
-[10] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[6][3]
-[11] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][10]
-[12] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[10]D[11][3]
+[13] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[6]D[7][3]
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
-[13] CpCNpq = D[12]1
+[14] CpCNpq = D[13]1
 
-[14] CCpCCqqrCCNrCCNstpCsr = D1[5]
-[15] CpCqCrp = DD[0][11][7]
-[16] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[11]1
-[17] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[3]
-[18] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1DD[17][0]11
-[19] CpCCNqCCNrsCNqCCNCtpuNCvCCwCvxCCNxCCNyzwCyxCrq = D[2][3]
-
-% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 781 steps
-[20] CCNppp = DDDD[14]1DDD[0]DDD1[15][0][16]DDD1DDD[0]D1[18][3]DD[0][17][3]DDD1[8]1[3][19]1DDD[0][15]DDD1DD[0]D1[16]DD[0]DDD1DDD1[6]111[3]1DDD1DDD1D[18][3]1[3]1[3][19]1DDD1D[12]DD[0][1]DD[0]DDD1DDD1[4]111[3]1[14]D[4]DD1[9]1
+% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 535 steps
+[15] CCNppp = DDDD[9]1DDD[0]DDD1DD[0][7][10][0]D[7]1DDD1DDD[0]D1DD1DD[4][0]11[3]DD[0][4][3]DDD1[11]1[3][3]11DDD1D[13]DD[0][2]DD[0]DDD1DDD1[5]111[3]1[9]D[5]DD1[12]1