S5=KM4B and S5=KM5

The 2 Axiomatizations

• S5=KM4B: PC + Necessitation + K + M + 4 + B
• S5=KM5: PC + Necessitation + K + M + 5
• Need prove only 4 and B from KM5, and 5 from KM4B

From S5=KM4B

• The problem file S5=KM4B_to_S5=KM5.p
• Proved axiom_5 ((only) by providing exactly the required parts of KM4B
  ( S5=KM4B_to_S5=KM5.reduced.p))

From S5=KM5

• The problem file S5=KM5_to_S5=KM4B.p
• Proved axiom_B