diff --git a/Pdl.lean b/Pdl.lean
index a87ecdb..c7533ce 100644
--- a/Pdl.lean
+++ b/Pdl.lean
@@ -6,7 +6,8 @@ import «Pdl».Vocab
 import «Pdl».Semantics
 import «Pdl».Star
 import «Pdl».Discon
-import «Pdl».Unravel
+-- import «Pdl».Unravel -- no longer used!
+import «Pdl».DagTableau
 import «Pdl».Tableau
 import «Pdl».Examples
 import «Pdl».Interpolation
diff --git a/Pdl/DagTableau.lean b/Pdl/DagTableau.lean
index 7a0ad5a..c028554 100644
--- a/Pdl/DagTableau.lean
+++ b/Pdl/DagTableau.lean
@@ -1,4 +1,5 @@
 import Mathlib.Data.Finset.Basic
+import Mathlib.Tactic.Linarith
 
 import Pdl.Syntax
 import Pdl.Discon
@@ -42,9 +43,7 @@ local notation "⌈" α "⌉" P => DagFormula.box α P
 local notation "⌈⌈" α "⌉⌉" P => DagFormula.boxes α P
 local notation "⌈" α "†⌉" P => DagFormula.dag α P
 
--- THE f FUNCTION
--- | Borzechowski's f function, sort of.
-
+-- | Borzechowski's function "f".
 def undag : DagFormula → Formula
   | ⊥ => ⊥
   | ~f => ~(undag f)
@@ -61,7 +60,6 @@ def inject : Formula → DagFormula
   | φ⋀ψ => inject φ ⋀ inject ψ
   | ⌈α⌉φ => ⌈α⌉(inject φ)
 
--- | Borzechowski's f function, sort of.
 @[simp]
 def containsDag : DagFormula → Bool
   | ⊥ => False
@@ -142,7 +140,7 @@ def dagNext : (Finset Formula × Option DagFormula) → Finset (Finset Formula 
   | (_, some _) => { }  -- bad catch-all fallback, and maybe wrong?
   | (_, none) => { }  -- maybe wrong?
 
-theorem mOfDagNode.isDec (x y : Finset Formula × Option DagFormula) (y_in : y ∈ dagNext x) :
+theorem mOfDagNode.isDec {x y : Finset Formula × Option DagFormula} (y_in : y ∈ dagNext x) :
     mOfDagNode y < mOfDagNode x := by
   rcases x with ⟨_, _|dfx⟩
   case none =>
@@ -151,29 +149,42 @@ theorem mOfDagNode.isDec (x y : Finset Formula × Option DagFormula) (y_in : y 
   case some =>
     simp [mOfDagNode]
     rcases y with ⟨_, _|dfy⟩
-    case none =>
-      simp
+    all_goals simp
     case some =>
-      simp
       cases dfx
-      all_goals (try simp [dagNext]; try cases y_in)
+      all_goals (try cases y_in)
       case neg g =>
         cases g
-        all_goals (try simp [dagNext]; try cases y_in)
-        case box a =>
+        all_goals (try cases y_in)
+        case box a f =>
           cases a
-          all_goals (cases dfy)
-          all_goals (simp [dagNext])
-          all_goals sorry
-          -- There must be a nicer way to do this?!
+          all_goals (simp [dagNext] at *)
+          case sequence =>
+            rcases y_in with ⟨l,r⟩
+            subst l
+            subst r
+            simp
+            linarith
+          case union a b =>
+            rcases y_in with ⟨l,r⟩|⟨l,r⟩
+            all_goals (subst l; subst r; simp; linarith)
+          case star a =>
+            rcases y_in with ⟨l,r⟩|⟨l,r⟩
+            all_goals (subst l; subst r; simp)
+          case test f =>
+            rcases y_in with ⟨l,r⟩
+            subst l
+            subst r
+            simp
 
 @[simp]
 def dagNextTransRefl : (Finset Formula × Option DagFormula) → Finset (Finset Formula × Option DagFormula) :=
-  ftr dagNext instDecidableEqProd mOfDagNode mOfDagNode.isDec
+  ftr dagNext instDecidableEqProd mOfDagNode @mOfDagNode.isDec
 
 instance modelCanSemImplyDagTabNodeNext {W : Type} : vDash (KripkeModel W × W) (Finset Formula × Option DagFormula) :=
   vDash.mk (λ ⟨M,w⟩ (fs, mf) => ∀ φ ∈ fs ∪ (mf.map undag).toFinset, evaluate M w φ)
 
+-- Similar to Borzechowski's Lemma 4
 theorem notStarSoundnessAux (a : Program) M (v w : W) (fs)
     (φ : DagFormula)
     (v_D : (M, v) ⊨ (fs, some (~⌈a⌉φ)))
@@ -206,7 +217,7 @@ theorem notStarSoundnessAux (a : Program) M (v w : W) (fs)
     case inl v_is_w =>
       use (fs, some (~φ))
       constructor
-      · unfold dagNextTransRefl; rw [ftr.iff]; right; simp; rw [ftr_iff]; simp
+      · unfold dagNextTransRefl; rw [ftr.iff]; right; simp; rw [ftr.iff]; simp
       · constructor
         · intro f
           aesop
@@ -275,15 +286,14 @@ theorem notStarSoundnessAux (a : Program) M (v w : W) (fs)
             · exact v_a_y
             · use u
               aesop
-    · -- TODO "If (2) ..."
-      -- subst v_is_u
+    · -- "If (2) ..."
       have := notStarSoundnessAux γ M u w S.1 φ -- not use "fs" here!
       specialize this _ u_γ_w w_nP
       · intro f
         sorry -- should be easy
       rcases this with ⟨Γ, Γ_in, v_Γ, split⟩
-      -- need transitivity here
       have also_in_prev : Γ ∈ dagNextTransRefl (fs, some (~⌈β;'γ⌉φ)) := by
+        -- Here we use transitivity of "being a successor" in a dagger tableau.
         apply ftr.Trans Γ S (fs, some (~⌈β;'γ⌉φ))
         · convert Γ_in
         · rw [ftr.iff]; simp; right; exact S_in
@@ -341,10 +351,27 @@ theorem notStarSoundnessAux (a : Program) M (v w : W) (fs)
       · intro f; aesop
       · right; aesop
 
-
 termination_by
   notStarSoundnessAux α M v w fs φ v_D v_a_w w_nP => mOfProgram α
 
+def dagEndNodes : (Finset Formula × Option DagFormula) → Finset (Finset Formula)
+  | (fs, none) => { fs }
+  | (fs, some df) => (dagNext (fs, some df)).attach.biUnion
+      (fun ⟨gsdf, h⟩ =>
+        have : mOfDagNode gsdf < mOfDagNode (fs, some df) := mOfDagNode.isDec h
+        dagEndNodes gsdf)
+termination_by
+  dagEndNodes fs => mOfDagNode fs
+decreasing_by simp_wf; assumption
+
+-- Similar to Borzechowski's Lemma 5
+-- (This is actually soundness AND invertibility.)
+theorem notStarSoundness (a : Program) (M : KripkeModel W) (v : W) (fs)
+    (φ : DagFormula)
+    :
+    ((M, v) ⊨ (fs, some (~⌈∗a⌉φ))) ↔ ∃ Γ ∈ dagEndNodes (fs, ~⌈∗a⌉φ), (M, v) ⊨ Γ := by
+
+    sorry
 
 -- -- -- BOXES -- -- --
 
@@ -374,3 +401,12 @@ termination_by
 -- how to ensure that union rule is "eventually" applied?
 -- May need to redefine DagTab to make it fully deterministic, even in box cases?
 -- Was not a problem for diamonds above.
+
+-- Analogon of Borzechowski's Lemma 5 for boxes, was missing.
+-- (This is actually soundness AND invertibility.)
+theorem starSoundness (a : Program) (M : KripkeModel W) (v : W) (fs)
+    (φ : DagFormula)
+    :
+    ((M, v) ⊨ (fs, some (⌈∗a⌉φ))) ↔ ∃ Γ ∈ dagEndNodes (fs, ⌈∗a⌉φ), (M, v) ⊨ Γ := by
+
+    sorry
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index d50d94e..1aa08da 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -8,7 +8,7 @@ import Pdl.Measures
 import Pdl.Setsimp
 import Pdl.Semantics
 import Pdl.Discon
-import Pdl.Unravel
+import Pdl.DagTableau -- replaces Pdl.Unravel
 
 -- HELPER FUNCTIONS
 
@@ -46,8 +46,8 @@ inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   | nUn {a b f} (h : (~⌈a⋓b⌉f) ∈ X) : localRule X { X \ {~⌈a ⋓ b⌉f} ∪ {~⌈a⌉f}
                                                     , X \ {~⌈a ⋓ b⌉f} ∪ {~⌈b⌉f} }
   -- STAR
-  | sta {X a f} (h : (⌈∗a⌉f) ∈ X) : localRule X ({ X \ {⌈∗a⌉f} } ⊎ (listsToSets (unravel (inject (⌈∗a⌉f)))))
-  | nSt {a f} (h : (~⌈∗a⌉f) ∈ X) : localRule X ({ X \ {~⌈∗a⌉f} } ⊎ (listsToSets (unravel (inject (~⌈∗a⌉f)))))
+  | sta {X a f} (h : (⌈∗a⌉f) ∈ X) : localRule X (dagEndNodes (X \ {⌈∗a⌉f}, inject (⌈∗a⌉f)))
+  | nSt {a f} (h : (~⌈∗a⌉f) ∈ X) : localRule X (dagEndNodes (X \ {~⌈∗a⌉f}, inject (~⌈∗a⌉f)))
 
   -- TODO which rules need and modify markings?
   -- TODO only apply * if there is a marking.
@@ -62,7 +62,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
   -- PROPOSITIONAL LOGIC
   case bot bot_in_a =>
     constructor
-    · intro ⟨Y,Y_in,w_Y⟩; simp at Y_in
+    · intro ⟨_, Y_in, _⟩; simp at Y_in
     · intro w_sat_a
       by_contra
       let w_sat_bot := w_sat_a ⊥ bot_in_a
@@ -199,105 +199,29 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
         case inr h_is_notf => rw [h_is_notf]; simp; exact not_w_g
   -- STAR RULES
   case nSt a f naSf_in_X =>
+    rw [Iff.comm]
+    convert notStarSoundness a M w (X \ {~⌈∗a⌉f}) (inject f) -- using Lemma 5
+    all_goals simp [vDash, undag, modelCanSemImplyDagTabNodeNext]
     constructor
-    · rintro ⟨Y, Y_in, MwY⟩ -- invertibility, should be easy
-      simp at Y_in
-      rcases Y_in with ⟨FS,FS_in,Y_def⟩
-      subst Y_def
-      intro g g_in_X
-      cases em (g = (~⌈∗a⌉f))
-      case inl g_is_nsSf =>
-        subst g_is_nsSf
-        simp
-        cases FS_in
-        case inl FS_is_nf =>
-          have : (FS : List Formula) = {~f} := by cases FS_is_nf; rfl; tauto
-          subst this
-          use w
-          constructor
-          · exact Relation.ReflTransGen.refl
-          · specialize MwY (~f)
-            simp at MwY
-            apply MwY
-            right
-            exact List.mem_of_mem_head? rfl
-        case inr FS_in_unrav =>
-
-          sorry
-      case inr g_neq_nsSf =>
-        apply MwY
-        simp
-        left
-        exact ⟨g_in_X, g_neq_nsSf⟩
-    · intro Mw_X -- soundness, needs Lemma
-      have w_adiamond_f := Mw_X (~⌈∗a⌉f) naSf_in_X
-      simp at w_adiamond_f
-      rcases w_adiamond_f with ⟨v, w_aS_v, v_nF⟩
-      -- NOTE: Borze also makes a distinction whether a is atomic. Not needed?
-      -- We still distinguish cases whether v = w
-      cases Classical.em (w = v)
-      case inl w_is_v =>
-        -- Same world, we can use the left branch.
-        subst w_is_v
-        use (X \ {~⌈∗a⌉f} ∪ {~f})
-        constructor
-        · apply union_elem_uplus
-          simp
-          unfold unravel
-          simp
-          use {~f}
-          constructor
-          · left
-            exact List.mem_of_mem_head? rfl
-          · rfl
-        · intro g g_in
-          simp at g_in
-          cases g_in
-          · tauto
-          case h.right.inr hyp =>
-            subst hyp
-            unfold evaluate
-            assumption
-      case inr w_neq_v =>
-        -- Different world, we use the right branch and Lemma 4 here:
-        have lemFour := likeLemmaFour M (∗ a) w v X.toList (inject f) w_neq_v
-        simp [vDash, modelCanSemImplyForm, modelCanSemImplyList] at lemFour
-        specialize lemFour _ w_aS_v v_nF
-        · intro g g_in
-          apply Mw_X
-          cases g_in
-          case a.inl => assumption
-          case a.inr h => convert naSf_in_X
-        rcases lemFour with ⟨Z, Z_in, Mw_ZX, ⟨as, nBasf_in, w_as_v⟩⟩
-        use (X \ {~⌈∗a⌉f}) ∪ Z.toFinset
-        constructor
-        · exact union_elem_uplus (by simp) (by simp; use Z)
-        · intro g g_in; simp at g_in; apply Mw_ZX; tauto
+    · intro Mw_X φ phi_in
+      apply Mw_X
+      aesop
+    · intro Mw_X φ phi_in
+      apply Mw_X
+      cases em (φ = (~⌈∗a⌉f))
+      all_goals aesop
   case sta a f aSf_in_X =>
+    rw [Iff.comm]
+    convert starSoundness a M w (X \ {⌈∗a⌉f}) (inject f) -- using the Box version of Lemma 5
+    all_goals simp [vDash, undag, modelCanSemImplyDagTabNodeNext, inject]
     constructor
-    · rintro ⟨Y, Y_in, w_Y⟩ -- invertibility, needs Lemma 4 3/4
-      simp at Y_in
-      rcases Y_in with ⟨Z, Z_in_unrav, Y_def⟩
-      subst Y_def
-      intro g g_in_X
-      cases Classical.em (g = (⌈∗a⌉f))
-      case inl g_def =>
-        subst g_def
-        simp
-        intro v w_a_v
-        have := lemmaFourAndThreeQuarters M -- use here?
-        sorry
-      case inr g_not =>
-        apply w_Y
-        simp
-        tauto
-    · intro w_X -- soundness, should be easy
-      simp
-      specialize w_X (⌈∗a⌉f) aSf_in_X
-      simp at w_X
-      -- simp
-      -- use (X \ {⌈∗a⌉f} ∪ (List.toFinset {f} ∪ List.toFinset a_1))
-      sorry
+    · intro Mw_X φ phi_in
+      apply Mw_X
+      aesop
+    · intro Mw_X φ phi_in
+      apply Mw_X
+      cases em (φ = (⌈∗a⌉f))
+      all_goals aesop
 
   -- OTHER PDL RULES
   case nTe φ ψ in_X =>
@@ -317,7 +241,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       simp
       intro f f_in
       simp at f_in
-      rcases f_in with f_is_phi | ⟨f_in_X, not_f⟩ | f_is_notPsi
+      rcases f_in with f_is_phi | ⟨f_in_X, _⟩ | f_is_notPsi
       · subst f_is_phi
         specialize w_X _ in_X
         simp at w_X
@@ -344,7 +268,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       simp
       intro f f_in
       simp at f_in
-      rcases f_in with ⟨f_in_X, not_f⟩ | f_is_notabPhi
+      rcases f_in with ⟨f_in_X, _⟩ | f_is_notabPhi
       · exact w_X _ f_in_X
       · subst f_is_notabPhi
         specialize w_X (~(⌈a;'b⌉φ)) nabf_in_X
@@ -367,7 +291,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       simp
       intro f f_in
       simp at f_in
-      rcases f_in with f_is_aPhi | ⟨f_in_X, f_is_not_aubPhi⟩ | f_is_bPhi
+      rcases f_in with f_is_aPhi | ⟨f_in_X, _⟩ | f_is_bPhi
       · subst f_is_aPhi
         specialize w_X (⌈a⋓b⌉φ) aubPhi_in_X
         simp at *
@@ -394,7 +318,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       simp
       intro f f_in
       simp at f_in
-      rcases f_in with ⟨f_in_X, not_f⟩ | f_is_abPhi
+      rcases f_in with ⟨f_in_X, _⟩ | f_is_abPhi
       · exact w_X _ f_in_X
       · subst f_is_abPhi
         specialize w_X (⌈a;'b⌉φ) abPhi_in_X
@@ -452,7 +376,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
         case inr f_def =>
           subst f_def
           exact w_Phi
-  case nUn a b φ naubPhi_in_X  => -- localRule X { X \ {~⌈a ⋓ b⌉φ} ∪ {~⌈a⌉φ}, X \ {~⌈a ⋓ b⌉φ} ∪ {~⌈b⌉φ} }
+  case nUn a b φ naubPhi_in_X => -- { X \ {~⌈a ⋓ b⌉φ} ∪ {~⌈a⌉φ}, X \ {~⌈a ⋓ b⌉φ} ∪ {~⌈b⌉φ} }
     constructor
     · rintro ⟨Y, Y_in, w_Y⟩
       simp at Y_in