Theory Splay_Tree_Analysis

subsection "Splay Tree Analysis"

theory Splay_Tree_Analysis
imports
  Splay_Tree_Analysis_Base
  Amortized_Framework
begin

subsubsection "Analysis of splay"

definition A_splay :: "'a::linorder ⇒ 'a tree ⇒ real" where
"A_splay a t = T_splay a t + Φ(splay a t) - Φ t"

text‹The following lemma is an attempt to prove a generic lemma that covers
both zig-zig cases. However, the lemma is not as nice as one would like.
Hence it is used only once, as a demo. Ideally the lemma would involve
function @{const A_splay}, but that is impossible because this involves @{const splay}
and thus depends on the ordering. We would need a truly symmetric version of @{const splay}
that takes the ordering as an explicit argument. Then we could define
all the symmetric cases by one final equation
\<^prop>‹splay2 less t = splay2 (λx y. Not (less x y)) (mirror t)›.
This would simplify the code and the proofs.›

lemma zig_zig: fixes lx x rx lb b rb a ra u lb1 lb2
defines [simp]: "X == Node lx (x) rx" defines[simp]: "B == Node lb b rb"
defines [simp]: "t == Node B a ra" defines [simp]: "A' == Node rb a ra"
defines [simp]: "t' == Node lb1 u (Node lb2 b A')"
assumes hyps: "lb ≠ ⟨⟩" and IH: "T_splay x lb + Φ lb1 + Φ lb2 - Φ lb ≤ 2 * φ lb - 3 * φ X + 1" and
 prems: "size lb = size lb1 + size lb2 + 1" "X ∈ subtrees lb"
shows "T_splay x lb + Φ t' - Φ t ≤ 3 * (φ t - φ X)"
proof -
  define B' where [simp]: "B' = Node lb2 b A'"
  have "T_splay x lb + Φ t' - Φ t = T_splay x lb + Φ lb1 + Φ lb2 - Φ lb + φ B' + φ A' - φ B"
    using prems
    by(auto simp: A_splay_def size_if_splay algebra_simps in_set_tree_if split: tree.split)
  also have "… ≤ 2 * φ lb + φ B' + φ A' - φ B - 3 * φ X + 1"
    using IH prems(2) by(auto simp: algebra_simps)
  also have "… ≤ φ lb + φ B' + φ A' - 3 * φ X + 1" by(simp)
  also have "… ≤ φ B' + 2 * φ t - 3 * φ X "
    using prems ld_ld_1_less[of "size1 lb" "size1 A'"]
    by(simp add: size_if_splay)
  also have "… ≤ 3 * φ t - 3 * φ X"
    using prems by(simp add: size_if_splay)
  finally show ?thesis by simp
qed

lemma A_splay_ub: "⟦ bst t; Node l x r : subtrees t ⟧
  ⟹ A_splay x t ≤ 3 * (φ t - φ(Node l x r)) + 1"
proof(induction x t rule: splay.induct)
  case 1 thus ?case by simp
next
  case 2 thus ?case by (auto simp: A_splay_def)
next
  case 4 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case 5 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case 7 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case 10 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case 12 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case 13 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
  case (3 x b A B CD)
  (* A readable proof *)
  let ?t = "⟨⟨A, x, B⟩, b, CD⟩"
  let ?t' = "⟨A, x, ⟨B, b, CD⟩⟩"
  have *: "l = A ∧ r = B" using "3.prems" by(fastforce dest: in_set_tree_if)
  have "A_splay x ?t = 1 + Φ ?t' - Φ ?t" using "3.hyps" by (simp add: A_splay_def)
  also have "… = 1 + φ ?t' + φ ⟨B, b, CD⟩  - φ ?t - φ ⟨A, x, B⟩" by(simp)
  also have "… = 1 + φ ⟨B, b, CD⟩ - φ ⟨A, x, B⟩" by(simp)
  also have "… ≤  1 + φ ?t - φ(Node A x B)"
    using log_le_cancel_iff[of 2 "size1(Node B b CD)" "size1 ?t"] by (simp)
  also have "… ≤ 1 + 3 * (φ ?t - φ(Node A x B))"
    using log_le_cancel_iff[of 2 "size1(Node A x B)" "size1 ?t"] by (simp)
  finally show ?case using * by simp
next
  case (9 b x AB C D)
  (* An automatic proof *)
  let ?A = "⟨AB, b, ⟨C, x, D⟩⟩"
  have "x ∉ set_tree AB" using "9.prems"(1) by auto
  with 9 show ?case using
    log_le_cancel_iff[of 2 "size1(Node AB b C)" "size1 ?A"]
    log_le_cancel_iff[of 2 "size1(Node C x D)" "size1 ?A"]
    by (auto simp: A_splay_def algebra_simps simp del:log_le_cancel_iff)
next
  case (6 x a b A B C)
  hence *: "⟨l, x, r⟩ ∈ subtrees A" by(fastforce dest: in_set_tree_if)
  obtain A1 a' A2 where sp: "splay x A = Node A1 a' A2"
    using splay_not_Leaf[OF ‹A ≠ Leaf›] by blast
  let ?X = "Node l x r" let ?AB = "Node A a B"  let ?ABC = "Node ?AB b C"
  let ?A' = "Node A1 a' A2"
  let ?BC = "Node B b C"  let ?A2BC = "Node A2 a ?BC" let ?A1A2BC = "Node A1 a' ?A2BC"
  have 0: "φ ?A1A2BC = φ ?ABC" using sp by(simp add: size_if_splay)
  have 1: "Φ ?A1A2BC - Φ ?ABC = Φ A1 + Φ A2 + φ ?A2BC + φ ?BC - Φ A - φ ?AB"
    using 0 by (simp)
  have "A_splay x ?ABC = T_splay x A + 1 + Φ ?A1A2BC - Φ ?ABC"
    using "6.hyps" sp by(simp add: A_splay_def)
  also have "… = T_splay x A + 1 + Φ A1 + Φ A2 + φ ?A2BC + φ ?BC - Φ A - φ ?AB"
    using 1 by simp
  also have "… = T_splay x A + Φ ?A' - φ ?A' - Φ A + φ ?A2BC + φ ?BC - φ ?AB + 1"
    by(simp)
  also have "… = A_splay x A + φ ?A2BC + φ ?BC - φ ?AB - φ ?A' + 1"
    using sp by(simp add: A_splay_def)
  also have "… ≤ 3 * φ A + φ ?A2BC + φ ?BC - φ ?AB - φ ?A' - 3 * φ ?X + 2"
    using "6.IH" "6.prems"(1) * by(simp)
  also have "… = 2 * φ A + φ ?A2BC + φ ?BC - φ ?AB - 3 * φ ?X + 2"
    using sp by(simp add: size_if_splay)
  also have "… < φ A + φ ?A2BC + φ ?BC - 3 * φ ?X + 2" by(simp)
  also have "… < φ ?A2BC + 2 * φ ?ABC - 3 * φ ?X + 1"
    using sp ld_ld_1_less[of "size1 A" "size1 ?BC"]
    by(simp add: size_if_splay)
  also have "… < 3 * φ ?ABC - 3 * φ ?X + 1"
    using sp by(simp add: size_if_splay)
  finally show ?case by simp
next
  case (8 a x b B A C)
  hence *: "⟨l, x, r⟩ ∈ subtrees B" by(fastforce dest: in_set_tree_if)
  obtain B1 b' B2 where sp: "splay x B = Node B1 b' B2"
     using splay_not_Leaf[OF ‹B ≠ Leaf›] by blast
  let ?X = "Node l x r" let ?AB = "Node A a B"  let ?ABC = "Node ?AB b C"
  let ?B' = "Node B1 b' B2"
  let ?AB1 = "Node A a B1"  let ?B2C = "Node B2 b C" let ?AB1B2C = "Node ?AB1 b' ?B2C"
  have 0: "φ ?AB1B2C = φ ?ABC" using sp by(simp add: size_if_splay)
  have 1: "Φ ?AB1B2C - Φ ?ABC = Φ B1 + Φ B2 + φ ?AB1 + φ ?B2C - Φ B - φ ?AB"
    using 0 by (simp)
  have "A_splay x ?ABC = T_splay x B + 1 + Φ ?AB1B2C - Φ ?ABC"
    using "8.hyps" sp by(simp add: A_splay_def)
  also have "… = T_splay x B + 1 + Φ B1 + Φ B2 + φ ?AB1 + φ ?B2C - Φ B - φ ?AB"
    using 1 by simp
  also have "… = T_splay x B + Φ ?B' - φ ?B' - Φ B + φ ?AB1 + φ ?B2C - φ ?AB + 1"
    by simp
  also have "… = A_splay x B + φ ?AB1 + φ ?B2C - φ ?AB - φ ?B' + 1"
    using sp by (simp add: A_splay_def)
  also have "… ≤ 3 * φ B + φ ?AB1 + φ ?B2C - φ ?AB - φ ?B' - 3 * φ ?X + 2"
    using "8.IH" "8.prems"(1) * by(simp)
  also have "… = 2 * φ B + φ ?AB1 + φ ?B2C - φ ?AB - 3 * φ ?X + 2"
    using sp by(simp add: size_if_splay)
  also have "… < φ B + φ ?AB1 + φ ?B2C - 3 * φ ?X + 2" by(simp)
  also have "… < φ B + 2 * φ ?ABC - 3 * φ ?X + 1"
    using sp ld_ld_1_less[of "size1 ?AB1" "size1 ?B2C"]
    by(simp add: size_if_splay)
  also have "… < 3 * φ ?ABC - 3 * φ ?X + 1" by(simp)
  finally show ?case by simp
next
  case (11 b x c C A D)
  hence *: "⟨l, x, r⟩ ∈ subtrees C" by(fastforce dest: in_set_tree_if)
  obtain C1 c' C2 where sp: "splay x C = Node C1 c' C2"
    using splay_not_Leaf[OF ‹C ≠ Leaf›] by blast
  let ?X = "Node l x r" let ?CD = "Node C c D"  let ?ACD = "Node A b ?CD"
  let ?C' = "Node C1 c' C2"
  let ?C2D = "Node C2 c D"  let ?AC1 = "Node A b C1"
  have "A_splay x ?ACD = A_splay x C + φ ?C2D + φ ?AC1 - φ ?CD - φ ?C' + 1"
    using "11.hyps" sp
    by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
  also have "… ≤ 3 * φ C + φ ?C2D + φ ?AC1 - φ ?CD - φ ?C' - 3 * φ ?X + 2"
    using "11.IH" "11.prems"(1) * by(auto simp: algebra_simps)
  also have "… = 2 * φ C + φ ?C2D + φ ?AC1 - φ ?CD - 3 * φ ?X + 2"
    using sp by(simp add: size_if_splay)
  also have "… ≤ φ C + φ ?C2D + φ ?AC1 - 3 * φ ?X + 2" by(simp)
  also have "… ≤ φ C + 2 * φ ?ACD - 3 * φ ?X + 1"
    using sp ld_ld_1_less[of "size1 ?C2D" "size1 ?AC1"]
    by(simp add: size_if_splay algebra_simps)
  also have "… ≤ 3 * φ ?ACD - 3 * φ ?X + 1" by(simp)
  finally show ?case by simp
next
  case (14 a x b CD A B)
  hence 0: "x ∉ set_tree B ∧ x ∉ set_tree A"
    using "14.prems"(1) ‹b<x› by(auto)
  hence 1: "x ∈ set_tree CD" using "14.prems" ‹b<x› ‹a<x› by (auto)
  obtain C c D where sp: "splay x CD = Node C c D"
    using splay_not_Leaf[OF ‹CD ≠ Leaf›] by blast
  from zig_zig[of CD x D C l r _ b B a A] 14 sp 0
  show ?case by(auto simp: A_splay_def size_if_splay algebra_simps)
(* The explicit version:
  have "A_splay x ?A = A_splay x ?R + φ ?B' + φ ?A' - φ ?B - φ ?R' + 1"
    using "14.prems" 1 sp
    by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
  also have "… ≤ 3 * φ ?R + φ ?B' + φ ?A' - φ ?B - φ ?R' - 3 * φ ?X + 2"
    using 14 0 by(auto simp: algebra_simps)
  also have "… = 2 * φ rb + φ ?B' + φ ?A' - φ ?B - 3 * φ ?X + 2"
    using sp by(simp add: size_if_splay)
  also have "… ≤ φ ?R + φ ?B' + φ ?A' - 3 * φ ?X + 2" by(simp)
  also have "… ≤ φ ?B' + 2 * φ ?A - 3 * φ ?X + 1"
    using sp ld_ld_1_less[of "size1 ?R" "size1 ?A'"]
    by(simp add: size_if_splay algebra_simps)
  also have "… ≤ 3 * φ ?A - 3 * φ ?X + 1"
    using sp by(simp add: size_if_splay)
  finally show ?case by simp
*)
qed

lemma A_splay_ub2: assumes "bst t" "x : set_tree t"
shows "A_splay x t ≤ 3 * (φ t - 1) + 1"
proof -
  from assms(2) obtain l r where N: "Node l x r : subtrees t"
    by (metis set_treeE)
  have "A_splay x t ≤ 3 * (φ t - φ(Node l x r)) + 1" by(rule A_splay_ub[OF assms(1) N])
  also have "… ≤ 3 * (φ t - 1) + 1" by(simp add: field_simps)
  finally show ?thesis .
qed

lemma A_splay_ub3: assumes "bst t" shows "A_splay x t ≤ 3 * φ t + 1"
proof cases
  assume "t = Leaf" thus ?thesis by(simp add: A_splay_def)
next
  assume "t ≠ Leaf"
  from ex_in_set_tree[OF this assms] obtain x' where
    a': "x' ∈ set_tree t"  "splay x' t = splay x t"  "T_splay x' t = T_splay x t"
    by blast
  show ?thesis using A_splay_ub2[OF assms a'(1)] by(simp add: A_splay_def a')
qed


subsubsection "Analysis of insert"

lemma amor_insert: assumes "bst t"
shows "T_insert x t + Φ(Splay_Tree.insert x t) - Φ t ≤ 4 * log 2 (size1 t) + 2" (is "?l ≤ ?r")
proof cases
  assume "t = Leaf" thus ?thesis by(simp)
next
  assume "t ≠ Leaf"
  then obtain l e r where [simp]: "splay x t = Node l e r"
    by (metis tree.exhaust splay_Leaf_iff)
  let ?t = "real(T_splay x t)"
  let ?Plr = "Φ l + Φ r"  let ?Ps = "Φ t"
  let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
  have opt: "?t + Φ (splay x t) - ?Ps  ≤ 3 * log 2 (real (size1 t)) + 1"
    using A_splay_ub3[OF ‹bst t›, simplified A_splay_def, of x] by (simp)
  from less_linear[of e x]
  show ?thesis
  proof (elim disjE)
    assume "e=x"
    have nneg: "log 2 (1 + real (size t)) ≥ 0" by simp
    thus ?thesis using ‹t ≠ Leaf› opt ‹e=x›
      apply(simp add: algebra_simps) using nneg by arith
  next
    let ?L = "log 2 (real(size1 l) + 1)"
    assume "e < x" hence "e ≠ x" by simp
    hence "?l = (?t + ?Plr - ?Ps) + ?L + ?LR"
      using  ‹t ≠ Leaf› ‹e<x› by(simp)
    also have "?t + ?Plr - ?Ps ≤ 2 * log 2 ?slr + 1"
      using opt size_splay[of x t,symmetric] by(simp)
    also have "?L ≤ log 2 ?slr" by(simp)
    also have "?LR ≤ log 2 ?slr + 1"
    proof -
      have "?LR ≤ log 2 (2 * ?slr)" by (simp add:)
      also have "… ≤ log 2 ?slr + 1"
        by (simp add: log_mult del:distrib_left_numeral)
      finally show ?thesis .
    qed
    finally show ?thesis using size_splay[of x t,symmetric] by (simp)
  next
    let ?R = "log 2 (2 + real(size r))"
    assume "x < e" hence "e ≠ x" by simp
    hence "?l = (?t + ?Plr - ?Ps) + ?R + ?LR"
      using ‹t ≠ Leaf› ‹x < e› by(simp)
    also have "?t + ?Plr - ?Ps ≤ 2 * log 2 ?slr + 1"
      using opt size_splay[of x t,symmetric] by(simp)
    also have "?R ≤ log 2 ?slr" by(simp)
    also have "?LR ≤ log 2 ?slr + 1"
    proof -
      have "?LR ≤ log 2 (2 * ?slr)" by (simp add:)
      also have "… ≤ log 2 ?slr + 1"
        by (simp add: log_mult del:distrib_left_numeral)
      finally show ?thesis .
    qed
    finally show ?thesis using size_splay[of x t, symmetric] by simp
  qed
qed


subsubsection "Analysis of delete"

definition A_splay_max :: "'a::linorder tree ⇒ real" where
"A_splay_max t = T_splay_max t + Φ(splay_max t) - Φ t"

lemma A_splay_max_ub: "t ≠ Leaf ⟹ A_splay_max t ≤ 3 * (φ t - 1) + 1"
proof(induction t rule: splay_max.induct)
  case 1 thus ?case by (simp)
next
  case (2 A)
  thus ?case using one_le_log_cancel_iff[of 2 "size1 A + 1"]
    by (simp add: A_splay_max_def del: one_le_log_cancel_iff)
next
  case (3 l b rl c rr)
  show ?case
  proof cases
    assume "rr = Leaf"
    thus ?thesis
      using one_le_log_cancel_iff[of 2 "1 + size1 rl"]
        one_le_log_cancel_iff[of 2 "1 + size1 l + size1 rl"]
        log_le_cancel_iff[of 2 "size1 l + size1 rl" "1 + size1 l + size1 rl"]
     by (auto simp: A_splay_max_def field_simps
           simp del: log_le_cancel_iff one_le_log_cancel_iff)
  next
    assume "rr ≠ Leaf"
    then obtain l' u r' where sp: "splay_max rr = Node l' u r'"
      using splay_max_Leaf_iff tree.exhaust by blast
    hence 1: "size rr = size l' + size r' + 1"
      using size_splay_max[of rr,symmetric] by(simp)
    let ?C = "Node rl c rr"  let ?B = "Node l b ?C"
    let ?B' = "Node l b rl"  let ?C' = "Node ?B' c l'"
    have "A_splay_max ?B = A_splay_max rr + φ ?B' + φ ?C' - φ rr - φ ?C + 1" using "3.prems" sp 1
      by(auto simp add: A_splay_max_def)
    also have "… ≤ 3 * (φ rr - 1) + φ ?B' + φ ?C' - φ rr - φ ?C + 2"
      using 3 ‹rr ≠ Leaf› by auto
    also have "… = 2 * φ rr + φ ?B' + φ ?C' - φ ?C - 1" by simp
    also have "… ≤ φ rr + φ ?B' + φ ?C' - 1" by simp
    also have "… ≤ 2 * φ ?B + φ ?C' - 2"
      using ld_ld_1_less[of "size1 ?B'" "size1 rr"] by(simp add:)
    also have "… ≤ 3 * φ ?B - 2" using 1 by simp
    finally show ?case by simp
  qed
qed

lemma A_splay_max_ub3: "A_splay_max t ≤ 3 * φ t + 1"
proof cases
  assume "t = Leaf" thus ?thesis by(simp add: A_splay_max_def)
next
  assume "t ≠ Leaf"
  show ?thesis using A_splay_max_ub[OF ‹t ≠ Leaf›] by(simp)
qed

lemma amor_delete: assumes "bst t"
shows "T_delete a t + Φ(Splay_Tree.delete a t) - Φ t ≤ 6 * log 2 (size1 t) + 2"
proof (cases t)
  case Leaf thus ?thesis by(simp add: Splay_Tree.delete_def)
next
  case [simp]: (Node ls x rs)
  then obtain l e r where sp[simp]: "splay a (Node ls x rs) = Node l e r"
    by (metis tree.exhaust splay_Leaf_iff)
  let ?t = "real(T_splay a t)"
  let ?Plr = "Φ l + Φ r"  let ?Ps = "Φ t"
  let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
  let ?lslr = "log 2 (real (size ls) + (real (size rs) + 2))"
  have "?lslr ≥ 0" by simp
  have opt: "?t + Φ (splay a t) - ?Ps  ≤ 3 * log 2 (real (size1 t)) + 1"
    using A_splay_ub3[OF ‹bst t›, simplified A_splay_def, of a]
    by (simp add: field_simps)
  show ?thesis
  proof (cases "e=a")
    case False thus ?thesis
      using opt apply(simp add: Splay_Tree.delete_def field_simps)
      using ‹?lslr ≥ 0› by arith
  next
    case [simp]: True
    show ?thesis
    proof (cases l)
      case Leaf
      have 1: "log 2 (real (size r) + 2) ≥ 0" by(simp)
      show ?thesis
        using Leaf opt apply(simp add: Splay_Tree.delete_def field_simps)
        using 1 ‹?lslr ≥ 0› by arith
    next
      case (Node ll y lr)
      then obtain l' y' r' where [simp]: "splay_max (Node ll y lr) = Node l' y' r'"
      using splay_max_Leaf_iff tree.exhaust by blast
      have "bst l" using bst_splay[OF ‹bst t›, of a] by simp
      have "Φ r' ≥ 0" apply (induction r') by (auto)
      have optm: "real(T_splay_max l) + Φ (splay_max l) - Φ l  ≤ 3 * φ l + 1"
        using A_splay_max_ub3[of l, simplified A_splay_max_def] by (simp add: field_simps Node)
      have 1: "log 2 (2+(real(size l')+real(size r))) ≤ log 2 (2+(real(size l)+real(size r)))"
        using size_splay_max[of l] Node by simp
      have 2: "log 2 (2 + (real (size l') + real (size r'))) ≥ 0" by simp
      have 3: "log 2 (size1 l' + size1 r) ≤ log 2 (size1 l' + size1 r') + log 2 ?slr"
        apply simp using 1 2 by arith
      have 4: "log 2 (real(size ll) + (real(size lr) + 2)) ≤ ?lslr"
        using size_if_splay[OF sp] Node by simp
      show ?thesis using add_mono[OF opt optm] Node 3
        apply(simp add: Splay_Tree.delete_def field_simps)
        using 4 ‹Φ r' ≥ 0› by arith
    qed
  qed
qed


subsubsection "Overall analysis"

fun U where
"U Empty [] = 1" |
"U (Splay _) [t] = 3 * log 2 (size1 t) + 1" |
"U (Insert _) [t] = 4 * log 2 (size1 t) + 3" |
"U (Delete _) [t] = 6 * log 2 (size1 t) + 3"

interpretation Amortized
where arity = arity and exec = exec and inv = bst
and cost = cost and Φ = Φ and U = U
proof (standard, goal_cases)
  case (1 ss f) show ?case
  proof (cases f)
    case Empty thus ?thesis using 1 by auto
  next
    case (Splay a)
    then obtain t where "ss = [t]" "bst t" using 1 by auto
    with Splay bst_splay[OF ‹bst t›, of a] show ?thesis
      by (auto split: tree.split)
  next
    case (Insert a)
    then obtain t where "ss = [t]" "bst t" using 1 by auto
    with bst_splay[OF ‹bst t›, of a] Insert show ?thesis
      by (auto simp: splay_bstL[OF ‹bst t›] splay_bstR[OF ‹bst t›] split: tree.split)
  next
    case (Delete a)
    then obtain t where "ss = [t]" "bst t" using 1 by auto
    with 1 Delete show ?thesis by(simp add: bst_delete)
  qed
next
  case (2 t) thus ?case by (induction t) auto
next
  case (3 ss f)
  show ?case (is "?l ≤ ?r")
  proof(cases f)
    case Empty thus ?thesis using 3(2) by(simp add: A_splay_def)
  next
    case (Splay a)
    then obtain t where "ss = [t]" "bst t" using 3 by auto
    thus ?thesis using Splay A_splay_ub3[OF ‹bst t›] by(simp add: A_splay_def)
  next
    case [simp]: (Insert a)
    then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
    thus ?thesis using amor_insert[of t a] by auto
  next
    case [simp]: (Delete a)
    then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
    thus ?thesis using amor_delete[of t a] by auto
  qed
qed

end