Theory Splay_Tree_Analysis_Optimal

subsection "Splay Tree Analysis (Optimal)"

theory Splay_Tree_Analysis_Optimal
imports
  Splay_Tree_Analysis_Base
  Amortized_Framework
  "HOL-Library.Sum_of_Squares"
begin

text‹This analysis follows Schoenmakers~cite"Schoenmakers-IPL93".›

subsubsection "Analysis of splay"

locale Splay_Analysis =
fixes α :: real and β :: real
assumes a1[arith]: "α > 1"
assumes A1: "1  x; 1  y; 1  z 
 (x+y) * (y+z) powr β  (x+y) powr β * (x+y+z)"
assumes A2: "1  l'; 1  r'; 1  lr; 1  r 
   α * (l'+r') * (lr+r) powr β * (lr+r'+r) powr β
     (l'+r') powr β * (l'+lr+r') powr β * (l'+lr+r'+r)"
assumes A3: "1  l'; 1  r'; 1  ll; 1  r 
  α * (l'+r') * (l'+ll) powr β * (r'+r) powr β
   (l'+r') powr β * (l'+ll+r') powr β * (l'+ll+r'+r)"
begin

lemma nl2: " ll  1; lr  1; r  1  
  log α (ll + lr) + β * log α (lr + r)
   β * log α (ll + lr) + log α (ll + lr + r)"
apply(rule powr_le_cancel_iff[THEN iffD1, OF a1])
apply(simp add: powr_add mult.commute[of β] powr_powr[symmetric] A1)
done


definition φ :: "'a tree  'a tree  real" where
"φ t1 t2 = β * log α (size1 t1 + size1 t2)"

fun Φ :: "'a tree  real" where
"Φ Leaf = 0" |
"Φ (Node l _ r) = Φ l + Φ r + φ l r"

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

lemma A_simps[simp]: "A a (Node l a r) = 1"
 "a<b  A a (Node (Node ll a lr) b r) = φ lr r - φ lr ll + 1"
 "b<a  A a (Node l b (Node rl a rr)) = φ rl l - φ rr rl + 1"
by(auto simp add: A_def φ_def algebra_simps)


lemma A_ub: " bst t; Node la a ra : subtrees t 
   A a t  log α ((size1 t)/(size1 la + size1 ra)) + 1"
proof(induction a t rule: splay.induct)
  case 1 thus ?case by simp
next
  case 2 thus ?case by auto
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 b a lb rb ra)
  have "b  set_tree ra" using "3.prems"(1) by auto
  thus ?case using "3.prems"(1,2) nl2[of "size1 lb" "size1 rb" "size1 ra"]
    by (auto simp: φ_def log_divide algebra_simps)
next
  case (9 a b la lb rb)
  have "b  set_tree la" using "9.prems"(1) by auto
  thus ?case using "9.prems"(1,2) nl2[of "size1 rb" "size1 lb" "size1 la"]
    by (auto simp add: φ_def log_divide algebra_simps)
next
  case (6 x b a lb rb ra)
  hence 0: "x  set_tree rb  x  set_tree ra" using "6.prems"(1) by auto
  hence 1: "x  set_tree lb" using "6.prems" x<b by (auto)
  then obtain lu u ru where sp: "splay x lb = Node lu u ru"
    using "6.prems"(1,2) by(cases "splay x lb") auto
  have "b < a" using "6.prems"(1,2) by (auto)
  let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
  let ?rb = "real(size1 rb)"  let ?r = "real(size1 ra)"
  have "1 + log α (?lu + ?ru) + β * log α (?rb + ?r) + β * log α (?rb + ?ru + ?r) 
        β * log α (?lu + ?ru) + β * log α (?lu + ?rb + ?ru) + log α (?lu + ?rb + ?ru + ?r)" (is "?L?R")
  proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
    show "α powr ?L  α powr ?R" using A2[of ?lu ?ru ?rb ?r]
      by(simp add: powr_add add_ac mult.commute[of β] powr_powr[symmetric])
  qed
  thus ?case using 6 0 1 sp
    by(auto simp: A_def φ_def size_if_splay algebra_simps log_divide)
next
  case (8 b x a rb lb ra)
  hence 0: "x  set_tree lb  x  set_tree ra" using "8.prems"(1) by(auto)
  hence 1: "x  set_tree rb" using "8.prems" b<x x<a by (auto)
  then obtain lu u ru where sp: "splay x rb = Node lu u ru"
    using "8.prems"(1,2) by(cases "splay x rb") auto
  let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
  let ?lb = "real(size1 lb)" let ?r = "real(size1 ra)"
  have "1 + log α (?lu + ?ru) + β * log α (?lu + ?lb) + β * log α (?ru + ?r) 
        β * log α (?lu + ?ru) + β * log α (?lu + ?lb + ?ru) + log α (?lu + ?lb + ?ru + ?r)" (is "?L?R")
  proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
     show "α powr ?L  α powr ?R" using A3[of ?lu ?ru ?lb ?r]
       by(simp add: powr_add mult.commute[of β] powr_powr[symmetric])
  qed
  thus ?case using 8 0 1 sp
    by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
next
  case (11 a x b lb la rb)
  hence 0: "x  set_tree rb  x  set_tree la" using "11.prems"(1) by (auto)
  hence 1: "x  set_tree lb" using "11.prems" a<x x<b by (auto)
  then obtain lu u ru where sp: "splay x lb = Node lu u ru"
    using "11.prems"(1,2) by(cases "splay x lb") auto
  let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
  let ?l = "real(size1 la)"  let ?rb = "real(size1 rb)"
  have "1 + log α (?lu + ?ru) + β * log α (?lu + ?l) + β * log α (?ru + ?rb) 
        β * log α (?lu + ?ru) + β * log α (?lu + ?ru + ?rb) + log α (?lu + ?l + ?ru + ?rb)" (is "?L?R")
  proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
    show "α powr ?L  α powr ?R" using A3[of ?ru ?lu ?rb ?l]
      by(simp add: powr_add mult.commute[of β] powr_powr[symmetric])
        (simp add: algebra_simps)
  qed
  thus ?case using 11 0 1 sp
    by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
next
  case (14 a x b rb la lb)
  hence 0: "x  set_tree lb  x  set_tree la" using "14.prems"(1) by(auto)
  hence 1: "x  set_tree rb" using "14.prems" a<x b<x by (auto)
  then obtain lu u ru where sp: "splay x rb = Node lu u ru"
    using "14.prems"(1,2) by(cases "splay x rb") auto
  let ?la = "real(size1 la)"  let ?lb = "real(size1 lb)"
  let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
  have "1 + log α (?lu + ?ru) + β * log α (?la + ?lb) + β * log α (?lu + ?la + ?lb) 
        β * log α (?lu + ?ru) + β * log α (?lu + ?lb + ?ru) + log α (?lu + ?lb + ?ru + ?la)" (is "?L?R")
  proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
     show "α powr ?L  α powr ?R" using A2[of ?ru ?lu ?lb ?la]
       by(simp add: powr_add add_ac mult.commute[of β] powr_powr[symmetric])
  qed
  thus ?case using 14 0 1 sp
    by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
qed

lemma A_ub2: assumes "bst t" "a : set_tree t"
shows "A a t  log α ((size1 t)/2) + 1"
proof -
  from assms(2) obtain la ra where N: "Node la a ra : subtrees t"
    by (metis set_treeE)
  have "A a t  log α ((size1 t)/(size1 la + size1 ra)) + 1"
    by(rule A_ub[OF assms(1) N])
  also have "  log α ((size1 t)/2) + 1" by(simp add: field_simps)
  finally show ?thesis by simp
qed

lemma A_ub3: assumes "bst t" shows "A a t  log α (size1 t) + 1"
proof cases
  assume "t = Leaf" thus ?thesis by(simp add: A_def)
next
  assume "t  Leaf"
  from ex_in_set_tree[OF this assms] obtain a' where
    a': "a'  set_tree t"  "splay a' t = splay a t"  "T_splay a' t = T_splay a t"
    by blast
  have [arith]: "log α 2 > 0" by simp
  show ?thesis using A_ub2[OF assms a'(1)] by(simp add: A_def a' log_divide)
qed


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

lemma Am_simp3': " c<b; bst rr; rr  Leaf 
  Am (Node l c (Node rl b rr)) =
  (case splay_max rr of Node rrl _ rrr 
   Am rr + φ rrl (Node l c rl) + φ l rl - φ rl rr - φ rrl rrr + 1)"
by(auto simp: Am_def φ_def size_if_splay_max algebra_simps neq_Leaf_iff split: tree.split)

lemma Am_ub: " bst t; t  Leaf   Am t  log α ((size1 t)/2) + 1"
proof(induction t rule: splay_max.induct)
  case 1 thus ?case by (simp)
next
  case 2 thus ?case by (simp add: Am_def)
next
  case (3 l b rl c rr)
  show ?case
  proof cases
    assume "rr = Leaf"
    thus ?thesis
      using nl2[of 1 "size1 rl" "size1 l"] log_le_cancel_iff[of α 2 "2 + real(size rl)"]
      by(auto simp: Am_def φ_def log_divide field_simps
           simp del: log_le_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] by(simp)
    let ?l = "real (size1 l)" let ?rl = "real (size1 rl)"
    let ?l' = "real (size1 l')" let ?r' = "real (size1 r')"
    have "1 + log α (?l' + ?r') + β * log α (?l + ?rl) + β * log α (?l' + ?l + ?rl) 
      β * log α (?l' + ?r') + β * log α (?l' + ?rl + ?r') + log α (?l' + ?rl + ?r' + ?l)" (is "?L?R")
    proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
      show "α powr ?L  α powr ?R" using A2[of ?r' ?l' ?rl ?l]
        by(simp add: powr_add add.commute add.left_commute mult.commute[of β] powr_powr[symmetric])
    qed
    thus ?case using 3 sp 1 rr  Leaf
      by(auto simp add: Am_simp3' φ_def log_divide algebra_simps)
  qed
qed

lemma Am_ub3: assumes "bst t" shows "Am t  log α (size1 t) + 1"
proof cases
  assume "t = Leaf" thus ?thesis by(simp add: Am_def)
next
  assume "t  Leaf"
  have [arith]: "log α 2 > 0" by simp
  show ?thesis using Am_ub[OF assms t  Leaf] by(simp add: Am_def log_divide)
qed

end


subsubsection "Optimal Interpretation"

lemma mult_root_eq_root:
  "n>0  y  0  root n x * y = root n (x * (y ^ n))"
by(simp add: real_root_mult real_root_pos2)

lemma mult_root_eq_root2:
  "n>0  y  0  y * root n x = root n ((y ^ n) * x)"
by(simp add: real_root_mult real_root_pos2)

lemma powr_inverse_numeral:
  "0 < x  x powr (1 / numeral n) = root (numeral n) x"
by (simp add: root_powr_inverse)

lemmas root_simps = mult_root_eq_root mult_root_eq_root2 powr_inverse_numeral


lemma nl31: " (l'::real)  1; r'  1; lr  1; r  1  
  4 * (l' + r') * (lr + r)  (l' + lr + r' + r)^2"
by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + lr + ~1*r']^2))))")

lemma nl32: assumes "(l'::real)  1" "r'  1" "lr  1" "r  1"
shows "4 * (l' + r') * (lr + r) * (lr + r' + r)  (l' + lr + r' + r)^3"
proof -
  have 1: "lr + r' + r  l' + lr + r' + r" using assms by arith
  have 2: "0  (l' + lr + r' + r)^2" by (rule zero_le_power2)
  have 3: "0  lr + r' + r" using assms by arith
  from mult_mono[OF nl31[OF assms] 1 2 3] show ?thesis
    by(simp add: ac_simps numeral_eq_Suc)
qed

lemma nl3: assumes "(l'::real)  1" "r'  1" "lr  1" "r  1"
shows "4 * (l' + r')^2 * (lr + r) * (lr + r' + r)
        (l' + lr + r') * (l' + lr + r' + r)^3"
proof-
  have 1: "l' + r'  l' + lr + r'" using assms by arith
  have 2: "0  (l' + lr + r' + r)^3" using assms by simp
  have 3: "0  l' + r'" using assms by arith
  from mult_mono[OF nl32[OF assms] 1 2 3] show ?thesis
    unfolding power2_eq_square by (simp only: ac_simps)
qed


lemma nl41: assumes "(l'::real)  1" "r'  1" "ll  1" "r  1"
shows "4 * (l' + ll) * (r' + r)  (l' + ll + r' + r)^2"
using assms by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + ~1*ll + r']^2))))")

lemma nl42: assumes "(l'::real)  1" "r'  1" "ll  1" "r  1"
shows "4 * (l' + r') * (l' + ll) * (r' + r)  (l' + ll + r' + r)^3"
proof -
  have 1: "l' + r'  l' + ll + r' + r" using assms by arith
  have 2: "0  (l' + ll + r' + r)^2" by (rule zero_le_power2)
  have 3: "0  l' + r'" using assms by arith
  from mult_mono[OF nl41[OF assms] 1 2 3] show ?thesis
    by(simp add: ac_simps numeral_eq_Suc del: distrib_right_numeral)
qed

lemma nl4: assumes "(l'::real)  1" "r'  1" "ll  1" "r  1"
shows "4 * (l' + r')^2 * (l' + ll) * (r' + r)
     (l' + ll + r') * (l' + ll + r' + r)^3"
proof-
  have 1: "l' + r'  l' + ll + r'" using assms by arith
  have 2: "0  (l' + ll + r' + r)^3" using assms by simp
  have 3: "0  l' + r'" using assms by arith
  from mult_mono[OF nl42[OF assms] 1 2 3] show ?thesis
    unfolding power2_eq_square by (simp only: ac_simps)
qed

lemma cancel: "x>(0::real)  c * x ^ 2 * y * z  u * v  c * x ^ 3 * y * z  x * u * v"
by(simp add: power2_eq_square power3_eq_cube)

interpretation S34: Splay_Analysis "root 3 4" "1/3"
proof (standard, goal_cases)
  case 2 thus ?case
    by(simp add: root_simps)
      (auto simp: numeral_eq_Suc split_mult_pos_le intro!: mult_mono)
next
  case 3 thus ?case by(simp add: root_simps cancel nl3)
next
  case 4 thus ?case by(simp add: root_simps cancel nl4)
qed simp


lemma log4_log2: "log 4 x = log 2 x / 2"
proof -
  have "log 4 x = log (2^2) x" by simp
  also have " = log 2 x / 2" by(simp only: log_base_pow)
  finally show ?thesis .
qed

declare log_base_root[simp]

lemma A34_ub: assumes "bst t"
shows "S34.A a t  (3/2) * log 2 (size1 t) + 1"
proof -
  have "S34.A a t  log (root 3 4) (size1 t) + 1" by(rule S34.A_ub3[OF assms])
  also have " = (3/2) * log 2 (size t + 1) + 1" by(simp add: log4_log2)
  finally show ?thesis by simp
qed

lemma Am34_ub: assumes "bst t"
shows "S34.Am t  (3/2) * log 2 (size1 t) + 1"
proof -
  have "S34.Am t  log (root 3 4) (size1 t) + 1" by(rule S34.Am_ub3[OF assms])
  also have " = (3/2) * log 2 (size1 t) + 1" by(simp add: log4_log2)
  finally show ?thesis by simp
qed

subsubsection "Overall analysis"

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

interpretation Amortized
where arity = arity and exec = exec and inv = bst
and cost = cost and Φ = S34.Φ 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) show ?case by(induction t)(simp_all add: S34.φ_def)
next
  case (3 ss f)
  show ?case (is "?l  ?r")
  proof(cases f)
    case Empty thus ?thesis using 3(2) by(simp add: S34.A_def)
  next
    case (Splay a)
    then obtain t where "ss = [t]" "bst t" using 3 by auto
    thus ?thesis using S34.A_ub3[OF bst t] Splay
      by(simp add: S34.A_def log4_log2)
  next
    case [simp]: (Insert a)
    obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
    show ?thesis
    proof cases
      assume "t = Leaf" thus ?thesis by(simp add: S34.φ_def log4_log2)
    next
      assume "t  Leaf"
      then obtain l e r where [simp]: "splay a t = Node l e r"
        by (metis tree.exhaust splay_Leaf_iff)
      let ?t = "real(T_splay a t)"
      let ?Plr = "S34.Φ l + S34.Φ r"  let ?Ps = "S34.Φ t"
      let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
      have opt: "?t + S34.Φ (splay a t) - ?Ps   3/2 * log 2 (real (size1 t)) + 1"
        using S34.A_ub3[OF bst t, simplified S34.A_def, of a]
        by (simp add: log4_log2)
      from less_linear[of e a]
      show ?thesis
      proof (elim disjE)
        assume "e=a"
        have nneg: "log 2 (1 + real (size t))  0" by simp
        thus ?thesis using t  Leaf opt e=a
          apply(simp add: field_simps) using nneg by arith
      next
        let ?L = "log 2 (real(size1 l) + 1)"
        assume "e<a" hence "e  a" by simp
        hence "?l = (?t + ?Plr - ?Ps) + ?L / 2 + ?LR / 2"
          using t  Leaf e<a by(simp add: S34.φ_def log4_log2)
        also have "?t + ?Plr - ?Ps  log 2 ?slr + 1"
          using opt size_splay[of a t,symmetric]
          by(simp add: S34.φ_def log4_log2)
        also have "?L/2  log 2 ?slr / 2" by(simp)
        also have "?LR/2  log 2 ?slr / 2 + 1/2"
        proof -
          have "?LR/2  log 2 (2 * ?slr) / 2" by simp
          also have "  log 2 ?slr / 2 + 1/2"
            by (simp add: log_mult del:distrib_left_numeral)
          finally show ?thesis .
        qed
        finally show ?thesis using size_splay[of a t,symmetric] by simp
      next
        let ?R = "log 2 (2 + real(size r))"
        assume "a<e" hence "e  a" by simp
        hence "?l = (?t + ?Plr - ?Ps) + ?R / 2 + ?LR / 2"
          using  t  Leaf a<e by(simp add: S34.φ_def log4_log2)
        also have "?t + ?Plr - ?Ps  log 2 ?slr + 1"
          using opt size_splay[of a t,symmetric]
          by(simp add: S34.φ_def log4_log2)
        also have "?R/2  log 2 ?slr / 2" by(simp)
        also have "?LR/2  log 2 ?slr / 2 + 1/2"
        proof -
          have "?LR/2  log 2 (2 * ?slr) / 2" by simp
          also have "  log 2 ?slr / 2 + 1/2"
            by (simp add: log_mult del:distrib_left_numeral)
          finally show ?thesis .
        qed
        finally show ?thesis using size_splay[of a t,symmetric] by simp
      qed
    qed
  next
    case [simp]: (Delete a)
    obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
    show ?thesis
    proof (cases t)
      case Leaf thus ?thesis
        by(simp add: Splay_Tree.delete_def S34.φ_def log4_log2)
    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 = "S34.Φ l + S34.Φ r"  let ?Ps = "S34.Φ 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 + S34.Φ (splay a t) - ?Ps   3/2 * log 2 (real (size1 t)) + 1"
        using S34.A_ub3[OF bst t, simplified S34.A_def, of a]
        by (simp add: log4_log2 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 "S34.φ Leaf r  0" by(simp add: S34.φ_def)
          thus ?thesis using Leaf opt
            apply(simp add: Splay_Tree.delete_def field_simps)
            using ?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 "S34.Φ r'  0" apply (induction r') by (auto simp add: S34.φ_def)
          have optm: "real(T_splay_max l) + S34.Φ (splay_max l) - S34.Φ l
             3/2 * log 2 (real (size1 l)) + 1"
            using S34.Am_ub3[OF bst l, simplified S34.Am_def]
            by (simp add: log4_log2 field_simps Node)
          have 1: "log 4 (2+(real(size l')+real(size r))) 
            log 4 (2+(real(size l)+real(size r)))"
            using size_splay_max[of l] Node by simp
          have 2: "log 4 (2 + (real (size l') + real (size r')))  0" by simp
          have 3: "S34.φ l' r  S34.φ l' r' + S34.φ l r"
            apply(simp add: S34.φ_def) 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 S34.Φ r'  0 by arith
        qed
      qed
    qed
  qed
qed

end