In case anyone cares, I created a variant of pmproofs.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> based on axioms CCpqCCqrCpr,CCNppp,CpCNpq, which are
luk-1 <https://us.metamath.org/mpeuni/luk-1.html> ((P -> Q) -> ((Q -> R) -> (P -> R))) luk-2 <https://us.metamath.org/mpeuni/luk-2.html> ((~ P -> P) -> P) luk-3 <https://us.metamath.org/mpeuni/luk-3.html> (P -> (~ P -> Q)) in Metamath. I used the new '--rebase' feature of pmGenerator, and then proof compression. The latter was mainly due to an attempt of finding a shorter proof of ax-2 <https://us.metamath.org/mpeuni/ax-2.html> (i.e. *2.77) than the current 91-step derivation. (So far, I didn't find one.) Direct link: L-pmproofs.txt <https://xamidi.github.io/luk-pmproofs/L-pmproofs.txt> [repo <https://github.com/xamidi/luk-pmproofs>] The repo is open for contributions. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/9e88ccb0-831b-4336-8d30-2059f24f8175n%40googlegroups.com.
