subsection‹Tests with the deep embedding: semantic frame conditions› theory PMLinHOL_deep_further_tests_2 imports PMLinHOL_deep_tests 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 φ::PML ψ::PML abbreviation(input) "F1 ≡ (◇⇧d(◇⇧dφ)) ⊃⇧d ◇⇧dφ" ―‹holds in K4› abbreviation(input) "F2 ≡ (◇⇧d(□⇧dφ)) ⊃⇧d □⇧d(◇⇧dφ)" ―‹holds in KB› abbreviation(input) "F3 ≡ (◇⇧d(□⇧dφ)) ⊃⇧d □⇧dφ" ―‹holds in KB4› abbreviation(input) "F4 ≡ (□⇧d(◇⇧d(□⇧d(◇⇧dφ)))) ⊃⇧d □⇧d(◇⇧dφ)" ―‹holds in KB/K4› abbreviation(input) "F5 ≡ (◇⇧d(φ ∧⇧d (◇⇧dψ))) ⊃⇧d ((◇⇧dφ) ∧⇧d (◇⇧dψ))" ―‹holds in K4› abbreviation(input) "F6 ≡ ((□⇧d(φ ⊃⇧d ψ)) ∧⇧d (◇⇧d(□⇧d(¬⇧dψ)))) ⊃⇧d ¬⇧d(◇⇧dψ)" ―‹holds in KB4› abbreviation(input) "F7 ≡ (◇⇧dφ) ⊃⇧d (□⇧d(φ ∨⇧d ◇⇧dφ))" ―‹holds in KB4› abbreviation(input) "F8 ≡ (◇⇧d(□⇧dφ)) ⊃⇧d (φ ∨⇧d ◇⇧dφ)" ―‹holds in KT/KB› abbreviation(input) "F9 ≡ ((□⇧d(◇⇧dφ)) ∧⇧d (□⇧d(◇⇧d(¬⇧d φ)))) ⊃⇧d ◇⇧d(◇⇧dφ)" ―‹holds in KT› abbreviation(input) "F10 ≡ ((□⇧d(φ ⊃⇧d □⇧dψ)) ∧⇧d (□⇧d(◇⇧d(¬⇧dψ)))) ⊃⇧d ¬⇧d(□⇧dψ)" ―‹holds in KT› declare imp_cong[cong del] experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F5)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F6)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F9)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧d F10)" ―‹nitpick[expect=none]› ―‹sledgehammer› ―‹none› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops end ―‹Summary of experiments: Nitpick: ctex=32 (with simp 8, without simp 24), none=56 (with simp 0, without simp 56), unknwn=72 (with simp 72, without simp 0) Sledgehammer: proof=70 (with simp 38, without simp 32), no prf=90 (with simp 42, without simp 48)› ―‹No conflicts› end