Theorem schema:

• Symbols are p, q and -.
• Axiom-defining scheme: If x consists only of hyphens, then xp-qx- is an axiom.
• Theorem production rule: If x, y and z consist only of hyphens, and xpyqz is known to be a theorem, then xpy-qz- is also a theorem.

Initial x:

Generate axiom Produce theorem