S5=S1-0M6S3M9B and S5=KM5

The 2 Axiomatizations

• S5=S1-0M6S3M9B: S1⁰ + M6 + S3 + M9 + B
• S5=KM5: PC + Necessitation + K + M + 5

From S5=S1-0M6S3M9B

• The problem file S5=S1-0M6S3M9B_to_S5=KM5.p
• Proved and_1, and_2, axiom_M

From S5=KM5

• The problem file S5=KM5_to_S5=S1-0M6S3M9B.p
• Proved axiom_s1_1, axiom_s1_2, axiom_s1_3, axiom_m6, axiom_m9, axiom_B, adjunction, modus_ponens_strict_implies
• HELP! Is substitution of strict equivalents provable in my encoding?
  (in ModalRuleDefns.ax)