Theory PMLinHOL_deep_further_tests_1

section‹Test Examples: Formula classification›
subsection‹Tests with the deep embedding: axiom schemata›
theory PMLinHOL_deep_further_tests_1
  imports PMLinHOL_deep_tests  
begin 
 ―‹What is the weakest modal logic in which the following test formulas F1-F10 are provable?›
 ―‹Test with schematic axioms›

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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  by (smt (z3) PML.simps(22))
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22)) 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F1" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22)) 
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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F2" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F3" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F4" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F5" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  by (smt (z3) PML.simps(22))
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F5" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  by (smt (z3) PML.simps(22))
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F5" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F5" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F6" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F6" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F6" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F7" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (smt (z3) PML.simps(22))
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf›
  oops
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F8" 
  ―‹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 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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F9" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof› 
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F9" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F9" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F9" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F10" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F10" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹proof›
  by (metis (mono_tags, lifting) PML.simps(22))  
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F10" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof› 
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf› 
  by (smt (verit) PML.simps(22,24))
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^d F10" 
  ―‹nitpick[expect=none]› ―‹sledgehammer›  ―‹none› ―‹proof› 
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›   ―‹unkn› ―‹no prf› 
  by (smt (verit) PML.simps(22,24))
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^d (□⇧^dφ) ⊃⇧^d □⇧^d(□⇧^dφ)) ⟶ ⟨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=16 (with simp 10, without simp 6), none=74 (with simp 0, without simp 74), unknwn=70 (with simp 70, without simp 0)
 Sledgehammer: proof=33 (with simp 16, without simp 17), no prf=127 (with simp 64, without simp 63)›

 ―‹No conflict›
end