Theory PMLinHOL_shallow_further_tests_1

subsection‹Tests with the (maximal) shallow embedding: axiom schemata›
theory PMLinHOL_shallow_further_tests_1 imports PMLinHOL_shallow_tests  
begin 
 ―‹What is the weakest modal logic in which the following test formulas F1-F10 are provable?›
 ―‹Test with schematic axioms›

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/K4›
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/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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1"
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F1" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F2" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F3" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F4" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit) NegS_def)
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F5" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (smt (verit, del_insts) NegS_def)
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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F6" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F7" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KTB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer› ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  oops 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma K4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F8" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹no prf›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F9" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F9" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F9" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F9" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F10" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma S4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F10" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis NegS_def) 
lemma KB4: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ∧ (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F10" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof› 
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis (lifting) BoxS_def NegS_def)
lemma KT: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s φ) ⟶ ⟨W,R,V⟩,w ⊨⇧^s F10" 
  ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  apply simp ―‹nitpick[expect=unknown]› ―‹sledgehammer›  ―‹unkn› ―‹proof›
  by (metis (lifting) BoxS_def NegS_def) 
lemma KB: "∀w:W. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s φ ⊃⇧^s □⇧^s(◇⇧^sφ)) ⟶ ⟨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. (∀φ. ⟨W,R,V⟩,w ⊨⇧^s (□⇧^sφ) ⊃⇧^s □⇧^s(□⇧^sφ)) ⟶ ⟨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=32 (with simp 16, without simp 16), none=0, unknwn=128 (with simp 64, without simp 64)
 Sledgehammer: proof=32 (with simp 24, without simp 8), no prf=128 (with simp 56, without simp 72)›

 ―‹No conflict›
end