xamidi
xamidi
/ pm.txt
Created
June 6, 2025 08:16
Proof summary of https://us.metamath.org/mmsolitaire/pmproofs.txt (version 26-Feb-2025) for use with https://github.com/xamidi/pmGenerator.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % Full summary: pmGenerator --transform data/pm.txt -f -n -t . -j 1 | |
| % - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u | |
| % - to file: pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u -o data/tmp.txt | |
| % Same steps: | |
| % - step counting: pmGenerator --transform data/pm.txt -f -n -t . -j -1 -p -2 -d | |
| % - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j -1 -u | |
| % Summary containing intermediate theorems with use counts of at least two: | |
| % - to file: pmGenerator --transform data/pm.txt -f -n -t . -o data/tmp.txt -d | |
| % (14702 bytes, in contrast to 14059 bytes here) |
xamidi
/ w2.txt from Prover9
Created
July 12, 2024 22:51
First constructive completeness proof ever found for Walsh's 2nd axiom. Proof summary equivalent to proofs in w2.out from https://pastebin.com/Ct3gwVEU.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % 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. | |
| % | |
| % Step counting: pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d | |
| % Compact (8364 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCCpCCqCprCCNrCCNstqCsruCvu,CpCCNqCCNrsCCtCCuCtvCCNvCCNwxuCwvqCrq,CpCqCrr,CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp,CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq,CpCqCrCsCtq,CpCqCrp,CCNCpCqrCCNstrCsCpCqr,CCNCNpqCCNrspCrCNpq,CNCpCqNrCsCtCur,CNCpCqrCsNr,CCNpCCNqrCNppCqp,CpCCNqqq,CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq,CCNCCpqqCCNrspCrCCpqq,CpCCNCpqCpqq,CCNCNpqpCNpq,CpCCNqNpq,CCNCpqCCNrsCNqNpCrCpq,CNNpCqp,CpCqNNCNpr,CpNNp,CCCpqCCrrsCqs,CpCqCNCrps,CpCqNNCrCsp,CpCCNCNqqCNqqq,CCCNpqNrCrCps,CCNpCCN |
xamidi
/ pm.txt
Last active
January 11, 2025 07:34
Proof summary of https://us.metamath.org/mmsolitaire/pmproofs.txt (version 15-Jun-2024) for use with https://github.com/xamidi/pmGenerator.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % Full summary: pmGenerator --transform data/pm.txt -f -n -t . -j 1 | |
| % - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u | |
| % - to file: pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u -o data/tmp.txt | |
| % Same steps: | |
| % - step counting: pmGenerator --transform data/pm.txt -f -n -t . -j -1 -p -2 -d | |
| % - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j -1 -u | |
| % Summary containing intermediate theorems with use counts of at least two: | |
| % - to file: pmGenerator --transform data/pm.txt -f -n -t . -o data/tmp.txt -d | |
| % (14569 bytes, in contrast to 13527 bytes here) |
xamidi
/ LongerLines.xml
Last active
June 19, 2024 08:53
My preferred C++ code style, importable into Eclipse CDT via Window.Preferences.C/C++."Code Style".Formatter."Import..." , or in project settings when Project.Properties."C/C++ General".Formatter."Enable project specific settings" is enabled via its "Import..." sibling.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | |
| <profiles version="1"> | |
| <profile kind="CodeFormatterProfile" name="LongerLines" version="1"> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_exception_specification" value="do not insert"/> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_after_pointer_in_method_declaration" value="insert"/> | |
| <setting id="org.eclipse.cdt.core.formatter.format_header_comment" value="true"/> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_parenthesized_expression" value="do not insert"/> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_for" value="do not insert"/> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_before_closing_brace_in_array_initializer" value="insert"/> | |
| <setting id="org.eclipse.cdt.core.formatter.insert_space_before_opening_paren_in_for" value="insert"/> |