subsection‹Tests with the (minimal) shallow embedding: semantic frame conditions› theory PMLinHOL_shallow_minimal_further_tests_2 imports PMLinHOL_shallow_minimal begin ―‹What is the weakest modal logic in which the following test formulas F1-F10 are provable?› ―‹Test with semantic conditions› abbreviation(input) refl ("𝗋") where "𝗋 ≡ λR. reflexive R" abbreviation(input) sym ("𝗌") where "𝗌 ≡ λR. symmetric R" abbreviation(input) tra ("𝗍") where "𝗍 ≡ λR. transitive R" consts φ::σ ψ::σ abbreviation(input) "F1 ≡ (◇⇧m(◇⇧mφ)) ⊃⇧m ◇⇧mφ" ―‹holds in K4› abbreviation(input) "F2 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m □⇧m(◇⇧mφ)" ―‹holds in KB› abbreviation(input) "F3 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m □⇧mφ" ―‹holds in KB4› abbreviation(input) "F4 ≡ (□⇧m(◇⇧m(□⇧m(◇⇧mφ)))) ⊃⇧m □⇧m(◇⇧mφ)" ―‹holds in KB› abbreviation(input) "F5 ≡ (◇⇧m(φ ∧⇧m (◇⇧mψ))) ⊃⇧m ((◇⇧mφ) ∧⇧m (◇⇧mψ))" ―‹holds in K4› abbreviation(input) "F6 ≡ ((□⇧m(φ ⊃⇧m ψ)) ∧⇧m (◇⇧m(□⇧m(¬⇧mψ)))) ⊃⇧m ¬⇧m(◇⇧mψ)" ―‹holds in KB4› abbreviation(input) "F7 ≡ (◇⇧mφ) ⊃⇧m (□⇧m(φ ∨⇧m ◇⇧mφ))" ―‹holds in KB4› abbreviation(input) "F8 ≡ (◇⇧m(□⇧mφ)) ⊃⇧m (φ ∨⇧m ◇⇧mφ)" ―‹holds in KT and in KB› abbreviation(input) "F9 ≡ ((□⇧m(◇⇧mφ)) ∧⇧m (□⇧m(◇⇧m(¬⇧m φ)))) ⊃⇧m ◇⇧m(◇⇧mφ)" ―‹holds in KT› abbreviation(input) "F10 ≡ ((□⇧m(φ ⊃⇧m □⇧mψ)) ∧⇧m (□⇧m(◇⇧m(¬⇧mψ)))) ⊃⇧m ¬⇧m(□⇧mψ)" ―‹holds in KT› declare imp_cong[cong del] experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "𝗋 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K: " (⊨⇧m F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "𝗋 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K4: " 𝗍 R ⟶ (⊨⇧m F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "𝗋 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "𝗋 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K4: " 𝗍 R ⟶ (⊨⇧m F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K: " (⊨⇧m F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "𝗋 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K: " (⊨⇧m F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "𝗋 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "𝗋 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: " 𝗌 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "𝗋 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: " 𝗌 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma K4: " 𝗍 R ⟶ (⊨⇧m F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "𝗋 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: " 𝗌 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma S4: "𝗋 R ∧ 𝗍 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB4: " 𝗌 R ∧ 𝗍 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "𝗋 R ∧ 𝗌 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KT: "𝗋 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› by metis lemma KB: " 𝗌 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: " 𝗍 R ⟶ (⊨⇧m F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: " (⊨⇧m F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end ―‹Summary of experiments: Nitpick: ctex=84 (with simp 42, without simp 42), none=76 (with simp 38, without simp 38), unknwn=0 Sledgehammer: proof=76 (with simp 38, without simp 38), no prf=84 (with simp 42, without simp 42) › ―‹No conflicts› end