subsection‹Tests with the (maximal) shallow embedding: semantic frame conditions› theory PMLinHOL_shallow_further_tests_2 imports PMLinHOL_shallow_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 φ::σ ψ::σ abbreviation(input) "F1 ≡ (◇⇧s(◇⇧sφ)) ⊃⇧s ◇⇧sφ" ―‹holds in K4› abbreviation(input) "F2 ≡ (◇⇧s(□⇧sφ)) ⊃⇧s □⇧s(◇⇧sφ)" ―‹holds in KB› abbreviation(input) "F3 ≡ (◇⇧s(□⇧sφ)) ⊃⇧s □⇧sφ" ―‹holds in KB4› abbreviation(input) "F4 ≡ (□⇧s(◇⇧s(□⇧s(◇⇧sφ)))) ⊃⇧s □⇧s(◇⇧sφ)" ―‹holds in KB› abbreviation(input) "F5 ≡ (◇⇧s(φ ∧⇧s (◇⇧sψ))) ⊃⇧s ((◇⇧sφ) ∧⇧s (◇⇧sψ))" ―‹holds in K4› abbreviation(input) "F6 ≡ ((□⇧s(φ ⊃⇧s ψ)) ∧⇧s (◇⇧s(□⇧s(¬⇧sψ)))) ⊃⇧s ¬⇧s(◇⇧sψ)" ―‹holds in KB4› abbreviation(input) "F7 ≡ (◇⇧sφ) ⊃⇧s (□⇧s(φ ∨⇧s ◇⇧sφ))" ―‹holds in KB4› abbreviation(input) "F8 ≡ (◇⇧s(□⇧sφ)) ⊃⇧s (φ ∨⇧s ◇⇧sφ)" ―‹holds in KT and in KB› abbreviation(input) "F9 ≡ ((□⇧s(◇⇧sφ)) ∧⇧s (□⇧s(◇⇧s(¬⇧s φ)))) ⊃⇧s ◇⇧s(◇⇧sφ)" ―‹holds in KT› abbreviation(input) "F10 ≡ ((□⇧s(φ ⊃⇧s □⇧sψ)) ∧⇧s (□⇧s(◇⇧s(¬⇧sψ)))) ⊃⇧s ¬⇧s(□⇧sψ)" ―‹holds in KT› declare imp_cong[cong del] experiment begin lemma S5: "∀w:W. 𝗋 R ∧ 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F1)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F2)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F2)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F3)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F3)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by metis lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by metis lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by metis lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by meson lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F4)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F5)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F5)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F6)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F6)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F7)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F7)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F8)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F9)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s F9)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹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 ⊨⇧s F10)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma S4: "∀w:W. 𝗋 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB4: "∀w:W. 𝗌 R ∧ 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma KTB: "∀w:W. 𝗋 R ∧ 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KT: "∀w:W. 𝗋 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹no prf› apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof› by blast lemma KB: "∀w:W. 𝗌 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K4: "∀w:W. 𝗍 R ⟶ (⟨W,R,V⟩,w ⊨⇧s F10)" ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› apply simp ―‹nitpick[expect=genuine]› ―‹sledgehammer› ―‹ctex› ―‹no prf› oops lemma K: "∀w:W. (⟨W,R,V⟩,w ⊨⇧s 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=0, unknwn=76 (with simp 38, without simp 38) Sledgehammer: proof=66 (with simp 38, without simp 28), no prf=94 (with simp 42, without simp 52)› ―‹No conflicts› end