Theory Sublinearity

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section ‹Sublinearity›

theory Sublinearity imports Embedding Healthiness LoopInduction begin

subsection ‹Nonrecursive Primitives›

text ‹Sublinearity of non-recursive programs is generally straightforward, and follows from the
alebraic properties of the underlying operations, together with healthiness.›

lemma sublinear_wp_Skip:
  "sublinear (wp Skip)"
  by(auto simp:wp_eval)

lemma sublinear_wp_Abort:
  "sublinear (wp Abort)"
  by(auto simp:wp_eval)

lemma sublinear_wp_Apply:
  "sublinear (wp (Apply f))"
  by(auto simp:wp_eval)

lemma sublinear_wp_Seq:
  fixes x::"'s prog"
  assumes slx: "sublinear (wp x)" and sly: "sublinear (wp y)"
      and hx:  "healthy (wp x)"   and hy:  "healthy (wp y)"
  shows "sublinear (wp (x ;; y))"
proof(rule sublinearI, simp add:wp_eval)
  fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  and a::real and b::real and c::real
  assume sP: "sound P" and sQ: "sound Q"
     and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"

  with slx hy have "a * wp x (wp y P) s + b * wp x (wp y Q) s ⊖ c ≤
                    wp x (λs. a * wp y P s + b * wp y Q s ⊖ c) s"
    by(blast intro:sublinearD)
  also {      
    from sP sQ nna nnb nnc sly
    have "⋀s. a * wp y P s + b * wp y Q s ⊖ c ≤
              wp y (λs. a * P s + b * Q s ⊖ c) s"
      by(blast intro:sublinearD)
    moreover from sP sQ hy
    have "sound (wp y P)" and "sound (wp y Q)" by(auto)
    moreover with nna nnb nnc
    have "sound (λs. a * wp y P s + b * wp y Q s ⊖ c)"
      by(auto intro!:sound_intros tminus_sound)
    moreover from sP sQ nna nnb nnc
    have "sound (λs. a * P s + b * Q s ⊖ c)"
      by(auto intro!:sound_intros tminus_sound)
    moreover with hy have "sound (wp y (λs. a * P s + b * Q s ⊖ c))"
      by(blast)
    ultimately
    have "wp x (λs. a * wp y P s + b * wp y Q s ⊖ c) s ≤
          wp x (wp y (λs. a * P s + b * Q s ⊖ c)) s"
      by(blast intro!:le_funD[OF mono_transD[OF healthy_monoD[OF hx]]])
  }
  finally show "a * wp x (wp y P) s + b * wp x (wp y Q) s ⊖ c ≤
                wp x (wp y (λs. a * P s + b * Q s ⊖ c)) s" .
qed

lemma sublinear_wp_PC:
  fixes x::"'s prog"
  assumes slx: "sublinear (wp x)" and sly: "sublinear (wp y)"
      and uP: "unitary P"
  shows "sublinear (wp (x ⇘P⇙⊕ y))"
proof(rule sublinearI, simp add:wp_eval)
  fix R::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  and a::real and b::real and c::real
  assume sR: "sound R" and sQ: "sound Q"
     and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"

  have "a * (P s * wp x Q s + (1 - P s) * wp y Q s) +
        b * (P s * wp x R s + (1 - P s) * wp y R s) ⊖ c =
        (P s * a * wp x Q s + (1 - P s) * a * wp y Q s) +
        (P s * b * wp x R s + (1 - P s) * b * wp y R s) ⊖ c"
    by(simp add:field_simps)
  also
  have "... = (P s * a * wp x Q s + P s * b * wp x R s) +
              ((1 - P s) * a * wp y Q s + (1 - P s) * b * wp y R s) ⊖ c"
    by(simp add:ac_simps)
  also
  have "... = P s * (a * wp x Q s + b * wp x R s) +
              (1 - P s) * (a * wp y Q s + b * wp y R s) ⊖
              (P s * c + (1 - P s) * c)"
    by(simp add:field_simps)
  also
  have "... ≤ (P s * (a * wp x Q s + b * wp x R s) ⊖ P s * c) +
              ((1 - P s) * (a * wp y Q s + b * wp y R s) ⊖ (1 - P s) * c)"
    by(rule tminus_add_mono)
  also {
      from uP have "0 ≤ P s" and "0 ≤ 1 - P s"
        by auto
      hence "(P s * (a * wp x Q s + b * wp x R s) ⊖ P s * c) +
             ((1 - P s) * (a * wp y Q s + b * wp y R s) ⊖ (1 - P s) * c) =
             P s * (a * wp x Q s + b * wp x R s ⊖ c) +
             (1 - P s) * (a * wp y Q s + b * wp y R s  ⊖ c)"
        by(simp add:tminus_left_distrib)
  }
  also {
    from sQ sR nna nnb nnc slx
    have "a * wp x Q s + b * wp x R s ⊖ c ≤
          wp x (λs. a * Q s + b * R s ⊖ c) s"
      by(blast)
    moreover
    from sQ sR nna nnb nnc sly
    have "a * wp y Q s + b * wp y R s ⊖ c ≤
          wp y (λs. a * Q s + b * R s ⊖ c) s"
      by(blast)
    moreover
    from uP have "0 ≤ P s" and "0 ≤ 1 - P s"
      by auto
    ultimately
    have "P s * (a * wp x Q s + b * wp x R s ⊖ c) +
          (1 - P s) * (a * wp y Q s + b * wp y R s  ⊖ c) ≤
          P s * wp x (λs. a * Q s + b * R s ⊖ c) s +
          (1 - P s) * wp y (λs. a * Q s + b * R s ⊖ c) s"
      by(blast intro:add_mono mult_left_mono)
  }
  finally
  show " a * (P s * wp x Q s + (1 - P s) * wp y Q s) +
         b * (P s * wp x R s + (1 - P s) * wp y R s) ⊖ c ≤
         P s * wp x (λs. a * Q s + b * R s ⊖ c) s +
         (1 - P s) * wp y (λs. a * Q s + b * R s ⊖ c) s" .
qed

lemma sublinear_wp_DC:
  fixes x::"'s prog"
  assumes slx: "sublinear (wp x)" and sly: "sublinear (wp y)"
  shows "sublinear (wp (x ⨅ y))"
proof(rule sublinearI, simp only:wp_eval)
  fix R::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  and a::real and b::real and c::real
  assume sR: "sound R" and sQ: "sound Q"
     and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"

  from nna nnb
  have "a * min (wp x Q s) (wp y Q s) +
        b * min (wp x R s) (wp y R s) ⊖ c =
        min (a * wp x Q s) (a * wp y Q s) +
        min (b * wp x R s) (b * wp y R s) ⊖ c"
    by(simp add:min_distrib)
  also
  have "... ≤ min (a * wp x Q s + b * wp x R s)
                  (a * wp y Q s + b * wp y R s) ⊖ c"
    by(auto intro!:tminus_left_mono)
  also
  have "... = min (a * wp x Q s + b * wp x R s ⊖ c)
                  (a * wp y Q s + b * wp y R s ⊖ c)"
    by(rule min_tminus_distrib)
  also {
    from slx sQ sR nna nnb nnc
    have "a * wp x Q s + b * wp x R s ⊖ c ≤
          wp x (λs. a * Q s + b * R s ⊖ c) s"
      by(blast)
    moreover
    from sly sQ sR nna nnb nnc
    have "a * wp y Q s + b * wp y R s ⊖ c ≤
          wp y (λs. a * Q s + b * R s ⊖ c) s"
      by(blast)
    ultimately
    have "min (a * wp x Q s + b * wp x R s ⊖ c)
              (a * wp y Q s + b * wp y R s ⊖ c) ≤
          min (wp x (λs. a * Q s + b * R s ⊖ c) s)
              (wp y (λs. a * Q s + b * R s ⊖ c) s)"
      by(auto)
  }
  finally show "a * min (wp x Q s) (wp y Q s) +
                b * min (wp x R s) (wp y R s) ⊖ c ≤
               min (wp x (λs. a * Q s + b * R s ⊖ c) s)
                   (wp y (λs. a * Q s + b * R s ⊖ c) s)" .
qed

text ‹As for continuity, we insist on a finite support.›
lemma sublinear_wp_SetPC:
  fixes p::"'a ⇒ 's prog"
  assumes slp: "⋀s a. a ∈ supp (P s) ⟹ sublinear (wp (p a))"
      and sum: "⋀s. (∑a∈supp (P s). P s a) ≤ 1"
      and nnP: "⋀s a. 0 ≤ P s a"
      and fin: "⋀s. finite (supp (P s))"
  shows "sublinear (wp (SetPC p P))"
proof(rule sublinearI, simp add:wp_eval)
  fix R::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  and a::real and b::real and c::real
  assume sR: "sound R" and sQ: "sound Q"
     and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"
  have "a * (∑a'∈supp (P s). P s a' * wp (p a') Q s) +
        b * (∑a'∈supp (P s). P s a' * wp (p a') R s) ⊖ c =
        (∑a'∈supp (P s). P s a' * (a * wp (p a') Q s + b * wp (p a') R s)) ⊖ c"
    by(simp add:field_simps sum_distrib_left sum.distrib)
  also have "... ≤
             (∑a'∈supp (P s). P s a' * (a * wp (p a') Q s + b * wp (p a') R s)) ⊖
             (∑a'∈supp (P s). P s a' * c)"
  proof(rule tminus_right_antimono)
    have "(∑a'∈supp (P s). P s a' * c) ≤ (∑a'∈supp (P s). P s a') * c"
      by(simp add:sum_distrib_right)
    also from sum and nnc have "... ≤ 1 * c"
      by(rule mult_right_mono)
    finally show "(∑a'∈supp (P s). P s a' * c) ≤ c" by(simp)
  qed
  also from fin
  have "... ≤ (∑a'∈supp (P s). P s a' * (a * wp (p a') Q s + b * wp (p a') R s) ⊖ P s a' * c)"
    by(blast intro:tminus_sum_mono)
  also have "... = (∑a'∈supp (P s). P s a' * (a * wp (p a') Q s + b * wp (p a') R s ⊖ c))"
    by(simp add:nnP tminus_left_distrib)
  also {
    from slp sQ sR nna nnb nnc
    have "⋀a'. a' ∈ supp (P s) ⟹ a * wp (p a') Q s + b * wp (p a') R s ⊖ c ≤
                                    wp (p a') (λs. a * Q s + b * R s ⊖ c) s"
      by(blast)
    with nnP
    have "(∑a'∈supp (P s). P s a' * (a * wp (p a') Q s + b * wp (p a') R s ⊖ c)) ≤
          (∑a'∈supp (P s). P s a' * wp (p a') (λs. a * Q s + b * R s ⊖ c) s)"
      by(blast intro:sum_mono mult_left_mono)
  }
  finally
  show "a * (∑a'∈supp (P s). P s a' * wp (p a') Q s) +
        b * (∑a'∈supp (P s). P s a' * wp (p a') R s) ⊖ c ≤
        (∑a'∈supp (P s). P s a' * wp (p a') (λs. a * Q s + b * R s ⊖ c) s)" .
qed

lemma sublinear_wp_SetDC:
  fixes p::"'a ⇒ 's prog"
  assumes slp: "⋀s a. a ∈ S s ⟹ sublinear (wp (p a))"
      and hp:  "⋀s a. a ∈ S s ⟹ healthy (wp (p a))"
      and ne:  "⋀s. S s ≠ {}"
  shows "sublinear (wp (SetDC p S))"
proof(rule sublinearI, simp add:wp_eval, rule cInf_greatest)
  fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s and x y
  and a::real and b::real and c::real
  assume sP: "sound P" and sQ: "sound Q"
     and nna: "0 ≤ a" and nnb: "0 ≤ b" and nnc: "0 ≤ c"

  from ne show "(λpr. wp (p pr) (λs. a * P s + b * Q s ⊖ c) s) ` S s ≠ {}" by(auto)

  assume yin: "y ∈ (λpr. wp (p pr) (λs. a * P s + b * Q s ⊖ c) s) ` S s"
  then obtain x where xin: "x ∈ S s" and rwy: "y = wp (p x) (λs. a * P s + b * Q s ⊖ c) s"
    by(auto)

  from xin hp sP nna
  have "a * Inf ((λa. wp (p a) P s) ` S s) ≤ a * wp (p x) P s"
    by(intro mult_left_mono[OF cInf_lower] bdd_belowI[where m=0], blast+)
  moreover from xin hp sQ nnb
  have "b * Inf ((λa. wp (p a) Q s) ` S s) ≤ b * wp (p x) Q s"
    by(intro mult_left_mono[OF cInf_lower] bdd_belowI[where m=0], blast+)
  ultimately
  have "a * Inf ((λa. wp (p a) P s) ` S s) +
        b * Inf ((λa. wp (p a) Q s) ` S s) ⊖ c ≤
        a * wp (p x) P s + b * wp (p x) Q s ⊖ c"
    by(blast intro:tminus_left_mono add_mono)

  also from xin slp sP sQ nna nnb nnc
  have "... ≤ wp (p x) (λs. a * P s + b * Q s ⊖ c) s"
    by(blast)

  finally show "a * Inf ((λa. wp (p a) P s) ` S s) + b * Inf ((λa. wp (p a) Q s) ` S s) ⊖ c ≤ y"
    by(simp add:rwy)
qed

lemma sublinear_wp_Embed:
  "sublinear t ⟹ sublinear (wp (Embed t))"
  by(simp add:wp_eval)

lemma sublinear_wp_repeat:
  "⟦ sublinear (wp p); healthy (wp p) ⟧ ⟹ sublinear (wp (repeat n p))"
  by(induct n, simp_all add:sublinear_wp_Seq sublinear_wp_Skip healthy_wp_repeat)

lemma sublinear_wp_Bind:
  "⟦ ⋀s. sublinear (wp (a (f s))) ⟧ ⟹ sublinear (wp (Bind f a))"
  by(rule sublinearI, simp add:wp_eval, auto)

subsection ‹Sublinearity for Loops›

text ‹We break the proof of sublinearity loops into separate proofs of sub-distributivity and
sub-additivity.  The first follows by transfinite induction.›
lemma sub_distrib_wp_loop:
  fixes body::"'s prog"
  assumes sdb: "sub_distrib (wp body)"
      and hb:  "healthy (wp body)"
      and nhb: "nearly_healthy (wlp body)"
  shows "sub_distrib (wp (do G ⟶ body od))"
proof -
  have "∀P s. sound P ⟶ wp (do G ⟶ body od) P s ⊖ 1 ≤ 
                          wp (do G ⟶ body od) (λs. P s ⊖ 1) s"
  proof(rule loop_induct[OF hb nhb], safe)
    fix S::"('s trans × 's trans) set" and P::"'s expect" and s::'s
    assume saS: "∀x∈S. ∀P s. sound P ⟶ fst x P s ⊖ 1 ≤ fst x (λs. P s ⊖ 1) s"
       and sP: "sound P"
       and fS: "∀x∈S. feasible (fst x)"

    from sP have sPm: "sound (λs. P s ⊖ 1)" by(auto intro:tminus_sound)

    have nnSup: "⋀s. 0 ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s"
    proof(cases "S={}", simp add:Sup_trans_def Sup_exp_def)
      fix s
      assume "S ≠ {}"
      then obtain x where xin: "x∈S" by(auto)
      with fS sPm have "0 ≤ fst x (λs. P s ⊖ 1) s" by(auto)
      also from xin fS sPm have "... ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s"
        by(auto intro!: le_funD[OF Sup_trans_upper2])
      finally show "?thesis s" .
    qed

    have "⋀x s. fst x P s ≤ (fst x P s ⊖ 1) + 1" by(simp add:tminus_def)
    also from saS sP
    have "⋀x s. x∈S ⟹ (fst x P s ⊖ 1) + 1 ≤ fst x (λs. P s ⊖ 1) s + 1"
      by(auto intro:add_right_mono)
    also {
      from sP have "sound (λs. P s ⊖ 1)" by(auto intro:tminus_sound)
      with fS have "⋀x s. x∈S ⟹ fst x (λs. P s ⊖ 1) s + 1 ≤
                                   Sup_trans (fst ` S) (λs. P s ⊖ 1) s + 1"
        by(blast intro!: add_right_mono le_funD[OF Sup_trans_upper2])
    }
    finally have le: "⋀s. ∀x∈S. fst x P s ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s + 1"
      by(auto)
    moreover from nnSup have nn: "⋀s. 0 ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s + 1"
      by(auto intro:add_nonneg_nonneg)
    ultimately
    have leSup: "Sup_trans (fst ` S) P s ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s + 1"
      unfolding Sup_trans_def
      by(intro le_funD[OF Sup_exp_least], auto)

    show "Sup_trans (fst ` S) P s ⊖ 1 ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s"
    proof(cases "Sup_trans (fst ` S) P s ≤ 1", simp_all add:nnSup)
      from leSup have "Sup_trans (fst ` S) P s - 1 ≤
                       Sup_trans (fst ` S) (λs. P s ⊖ 1) s + 1 - 1"
        by(auto)
      thus "Sup_trans (fst ` S) P s - 1 ≤ Sup_trans (fst ` S) (λs. P s ⊖ 1) s" by(simp)
    qed
  next
    fix t::"'s trans" and P::"'s expect" and s::'s
    assume IH: "∀P s. sound P ⟶ t P s ⊖ 1 ≤ t (λa. P a ⊖ 1) s"
       and ft: "feasible t"
       and sP: "sound P"

     from sP have "sound (λs. P s ⊖ 1)" by(auto intro:tminus_sound)
     with ft have s2: "sound (t (λs. P s ⊖ 1))" by(auto)
     from sP ft have "sound (t P)" by(auto)
     hence s3: "sound (λs. t P s ⊖ 1)" by(auto intro!:tminus_sound)

    show "wp (body ;; Embed t ⇘« G »⇙⊕ Skip) P s ⊖ 1 ≤
          wp (body ;; Embed t ⇘« G »⇙⊕ Skip) (λa. P a ⊖ 1) s"
    proof(simp add:wp_eval)
      have "«G» s * wp body (t P) s + (1 - «G» s) * P s ⊖ 1 =
            «G» s * wp body (t P) s + (1 - «G» s) * P s ⊖ («G» s + (1 - «G» s))"
        by(simp)
      also have "... ≤ («G» s * wp body (t P) s ⊖ «G» s) +
                        ((1 - «G» s) * P s ⊖ (1 - «G» s))"
        by(rule tminus_add_mono)
      also have "... = «G» s * (wp body (t P) s ⊖ 1) + (1 - «G» s) * (P s ⊖ 1)"
        by(simp add:tminus_left_distrib)
      also {
        from ft sP have "wp body (t P) s ⊖ 1 ≤ wp body (λs. t P s ⊖ 1) s"
          by(auto intro:sub_distribD[OF sdb])
        also {
          from IH sP have "λs. t P s ⊖ 1 ⊩ t (λs. P s ⊖ 1)" by(auto)
          with sP ft s2 s3 have "wp body (λs. t P s ⊖ 1) s ≤ wp body (t (λs. P s ⊖ 1)) s"
            by(blast intro:le_funD[OF mono_transD, OF healthy_monoD, OF hb])
        }
        finally have "«G» s * (wp body (t P) s ⊖ 1) + (1 - «G» s) * (P s ⊖ 1) ≤
                      «G» s * wp body (t (λs. P s ⊖ 1)) s + (1 - «G» s) * (P s ⊖ 1)"
          by(auto intro:add_right_mono mult_left_mono)
      }
      finally show "«G» s * wp body (t P) s + (1 - «G» s) * P s ⊖ 1 ≤
                    «G» s * wp body (t (λs. P s ⊖ 1)) s + (1 - «G» s) * (P s ⊖ 1)" .
    qed
  next
    fix t t'::"'s trans" and P::"'s expect" and s::'s
    assume IH: "∀P s. sound P ⟶ t P s ⊖ 1 ≤ t (λa. P a ⊖ 1) s"
       and eq: "equiv_trans t t'" and sP: "sound P"

    from sP have "t' P s ⊖ 1 = t P s ⊖ 1" by(simp add:equiv_transD[OF eq])
    also from sP IH have "... ≤ t (λs. P s ⊖ 1) s" by(auto)
    also {
      from sP have "sound (λs. P s ⊖ 1)" by(simp add:tminus_sound)
      hence "t (λs. P s ⊖ 1) s = t' (λs. P s ⊖ 1) s" by(simp add:equiv_transD[OF eq])
    }
    finally show "t' P s ⊖ 1 ≤ t' (λs. P s ⊖ 1) s" .
  qed
  thus ?thesis by(auto intro!:sub_distribI)
qed

text ‹For sub-additivity, we again use the limit-of-iterates characterisation.  Firstly, all
iterates are sublinear:›
lemma sublinear_iterates:
  assumes hb: "healthy (wp body)"
      and sb: "sublinear (wp body)"
  shows "sublinear (iterates body G i)"
  by(induct i, auto intro!:sublinear_wp_PC sublinear_wp_Seq sublinear_wp_Skip sublinear_wp_Embed
                           assms healthy_intros iterates_healthy)

text ‹From this, sub-additivity follows for the limit (i.e. the loop), by appealing to the
property at all steps.›
lemma sub_add_wp_loop:
  fixes body::"'s prog"
  assumes sb: "sublinear (wp body)"
      and cb:  "bd_cts (wp body)"
      and hwp:  "healthy (wp body)"
  shows "sub_add (wp (do G ⟶ body od))"
proof
  fix P Q::"'s expect" and s::'s
  assume sP: "sound P" and sQ: "sound Q"

  from hwp cb sP have "(λi. iterates body G i P s) ⇢ wp do G ⟶ body od P s"
    by(rule loop_iterates)
  moreover
  from hwp cb sQ have "(λi. iterates body G i Q s) ⇢ wp do G ⟶ body od Q s"
    by(rule loop_iterates)
  ultimately
  have "(λi. iterates body G i P s + iterates body G i Q s) ⇢
        wp do G ⟶ body od P s + wp do G ⟶ body od Q s"
    by(rule tendsto_add)
  moreover {
    from sublinear_subadd[OF sublinear_iterates, OF hwp sb,
                          OF healthy_feasibleD[OF iterates_healthy, OF hwp]] sP sQ
    have "⋀i. iterates body G i P s + iterates body G i Q s ≤ iterates body G i (λs. P s + Q s) s"
      by(rule sub_addD)
  }
  moreover {
    from sP sQ have "sound (λs. P s + Q s)" by(blast intro:sound_intros)
    with hwp cb have "(λi. iterates body G i (λs. P s + Q s) s) ⇢
                           wp do G ⟶ body od (λs. P s + Q s) s"
      by(blast intro:loop_iterates)
  }
  ultimately
  show "wp do G ⟶ body od P s + wp do G ⟶ body od Q s ≤ wp do G ⟶ body od (λs. P s + Q s) s"
    by(blast intro:LIMSEQ_le)  
qed

lemma sublinear_wp_loop:
  fixes body::"'s prog"
  assumes hb:  "healthy (wp body)"
      and nhb: "nearly_healthy (wlp body)"
      and sb:  "sublinear (wp body)"
      and cb:  "bd_cts (wp body)"
  shows "sublinear (wp (do G ⟶ body od))"
   using sublinear_sub_distrib[OF sb] sublinear_subadd[OF sb]
         hb healthy_feasibleD[OF hb]
   by(iprover intro:sd_sa_sublinear[OF _ _ healthy_wp_loop[OF hb]]
                    sub_distrib_wp_loop sub_add_wp_loop assms)

lemmas sublinear_intros =
  sublinear_wp_Abort
  sublinear_wp_Skip
  sublinear_wp_Apply
  sublinear_wp_Seq
  sublinear_wp_PC
  sublinear_wp_DC
  sublinear_wp_SetPC
  sublinear_wp_SetDC
  sublinear_wp_Embed
  sublinear_wp_repeat
  sublinear_wp_Bind
  sublinear_wp_loop

end