readme: adjust formulation to fit previous commit

Author: xamidi

README.html

@@ -269,7 +269,7 @@
 <h1 id="xamidipmgenerator">@xamidi/pmGenerator</h1>
 <p><a href="https://doi.org/10.5281/zenodo.10931360"><img src="svg/zenodo.10931360.svg" alt="DOI"></a></p>
 <p>This tool can collect exhaustive sets of <a href="https://en.wikipedia.org/wiki/Condensed_detachment">condensed detachment</a> proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”</a> collection.<br>The D-rule combines unification with <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a> (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus <em>pmGenerator</em> covers all <a href="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> within <a href="https://en.wikipedia.org/wiki/Hilbert_system">Hilbert systems</a> based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.<br>There is a <a href="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information.</p>
-<p>Eligible for high-performance computing. If you have access to a powerful computer, you may use <em>pmGenerator</em> to further contribute to our knowledge regarding the <a href="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>. The following table exemplary shows progress that has already been made.</p>
+<p>Eligible for high-performance computing. If you have access to a powerful computer, you may use <em>pmGenerator</em> to further contribute to our knowledge regarding the <a href="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>. Progress that has already been made is exemplarily shown below.</p>
 <h6 id="freges-calculus-simplified-by-łukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz (<a href="svg/frege-1.svg">CpCqp</a>,<a href="svg/frege-2.svg">CCpCqrCCpqCpr</a>,<a href="svg/lukasiewicz-3.svg">CCNpNqCqp</a>) &nbsp;<small>[<a href="data/top1000SmallestConclusions_1to39Steps.txt">top1000</a>] [<a href="data/cardinalities.txt">cardinalities</a>] [<a href="https://us.metamath.org/mmsolitaire/pmproofs.txt">db</a>] [<a href="data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/!.def">customization info</a>]</small></h6>
 <details open><summary>Behavioral Graph &nbsp;<small>[<a href="svg/plot/default-bgraph_grayscale.svg">grayscale</a>]</small></summary>
 <a href="https://xamidi.github.io/pmGenerator/svg/plot/default-bgraph.svg"><img src="svg/plot/default-bgraph.svg" width="700"></a></details>

README.md

@@ -7,7 +7,7 @@ This tool can collect exhaustive sets of [condensed detachment](https://en.wikip
 The D-rule combines unification with [modus ponens](https://en.wikipedia.org/wiki/Modus_ponens) (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus *pmGenerator* covers all [syntactic consequences](https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence) within [Hilbert systems](https://en.wikipedia.org/wiki/Hilbert_system) based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.  
 There is a [discussion forum](https://github.com/xamidi/pmGenerator/discussions) for questions, ideas, challenges, and related information.
 
-Eligible for high-performance computing. If you have access to a powerful computer, you may use *pmGenerator* to further contribute to our knowledge regarding the [complexity of proof systems](https://en.wikipedia.org/wiki/Proof_complexity). The following table exemplary shows progress that has already been made.
+Eligible for high-performance computing. If you have access to a powerful computer, you may use *pmGenerator* to further contribute to our knowledge regarding the [complexity of proof systems](https://en.wikipedia.org/wiki/Proof_complexity). Progress that has already been made is exemplarily shown below.
 
 ###### Frege's calculus simplified by Łukasiewicz ([CpCqp](svg/frege-1.svg),[CCpCqrCCpqCpr](svg/frege-2.svg),[CCNpNqCqp](svg/lukasiewicz-3.svg)) &nbsp;<sup><sub>[[top1000](data/top1000SmallestConclusions_1to39Steps.txt)] [[cardinalities](data/cardinalities.txt)] [[db](https://us.metamath.org/mmsolitaire/pmproofs.txt)] [[customization info](data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/!.def)]</sub></sup>
 <details open><summary>Behavioral Graph &nbsp;<sup><sub>[<a href="svg/plot/default-bgraph_grayscale.svg">grayscale</a>]</sub></sup></summary>