Theory BIT_2comp_on2

theory BIT_2comp_on2
imports BIT Phase_Partitioning
(*  Title:       BIT is 1.75 competitive on lists of length 2
    Author:      Max Haslbeck
*)
section "BIT is 1.75 competitive on lists of length 2"

theory BIT_2comp_on2
imports BIT Phase_Partitioning
begin

subsection "auxliary lemmas"

subsubsection "‹E_bernoulli3›"

lemma E_bernoulli3: assumes "0<p"
    and "p<1"
    and "finite (set_pmf (bind_pmf (bernoulli_pmf p) f))"
    shows "E (bind_pmf (bernoulli_pmf p) f) = E(f True)*p + E(f False)*(1-p)" (is "?L = ?R")
proof -

  have T: "(∑a∈(⋃x. set_pmf (f x)). (a * pmf (f True) a))
            = E(f True)"
    unfolding E_def
    apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
      using assms apply(simp)
      using assms apply(simp add: set_pmf_bernoulli) apply blast
      using assms by(simp add: set_pmf_bernoulli mult_ac) 
  have F: "(∑a∈(⋃x. set_pmf (f x)). (a * pmf (f False) a))
            = E(f False)"
    unfolding E_def
    apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
      using assms apply(simp)
      using assms apply(simp add: set_pmf_bernoulli) apply blast
      using assms by(simp add: set_pmf_bernoulli mult_ac) 

  have "?L = (∑a∈(⋃x. set_pmf (f x)).
       a *
       (pmf (f True) a * p +
        pmf (f False) a * (1 - p)))"  
  unfolding E_def 
  apply(subst integral_measure_pmf[of "bind_pmf (bernoulli_pmf p) f"])
    using assms apply(simp)
    apply(simp)
    using assms apply(simp add: set_pmf_bernoulli )
    by(simp add: pmf_bind mult_ac)
  also have "… = (∑a∈(⋃x. set_pmf (f x)). (a * pmf (f True) a * p)
                                    + (a * pmf (f False) a * (1 - p)))"
    apply(rule sum.cong) apply(simp) by algebra
  also have "… = (∑a∈(⋃x. set_pmf (f x)). (a * pmf (f True) a * p))
                  + (∑a∈(⋃x. set_pmf (f x)). (a * pmf (f False) a * (1 - p)))"
    by (simp add: sum.distrib)
  also have "… = (∑a∈(⋃x. set_pmf (f x)). (a * pmf (f True) a)) * p
                  + (∑a∈(⋃x. set_pmf (f x)). (a * pmf (f False) a )) * (1 - p)"
    by (simp add: sum_distrib_right)    
  also have "… = ?R" unfolding T F by simp
  finally show ?thesis .
qed 


subsubsection "types of configurations"

definition "type0 init x y = do {
                  (a::bool) ← (bernoulli_pmf 0.5);
                  (b::bool) ← (bernoulli_pmf 0.5);
                  return_pmf  ([x,y], ([a,b],init))
                }"

definition "type1 init x y = do {
                  (a::bool) ← (bernoulli_pmf 0.5);
                  (b::bool) ← (bernoulli_pmf 0.5);
                  return_pmf ( if ~[a,b]!(index init x)∧[a,b]!(index init y) then ([y,x], ([a,b],init))
                         else ([x,y], ([a,b],init)))
                }"

definition "type3 init x y = do {
                  (a::bool) ← (bernoulli_pmf 0.5);
                  (b::bool) ← (bernoulli_pmf 0.5);
                  return_pmf ( if [a,b]!(index init x)∧~[a,b]!(index init y) then ([x,y], ([a,b],init))
                         else ([y,x], ([a,b],init)))
                }"

definition "type4 init x y = do {
                  (a::bool) ← (bernoulli_pmf 0.5);
                  (b::bool) ← (bernoulli_pmf 0.5);
                  return_pmf ( if ~[a,b]!(index init y) then ([x,y], ([a,b],init))
                         else ([y,x], ([a,b],init)))
                }"

definition "BIT_inv s x i == (s = (type0 i x (hd (filter (λy. y≠x) i) )))"

lemma BIT_inv2: "x≠y ⟹ z∈{x,y} ⟹ BIT_inv s z [x,y] = (s= type0 [x,y] z (other z x y))"
  unfolding BIT_inv_def by(auto simp add: other_def)

subsubsection "cost of BIT"

lemma costBIT_0x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type0 [x0, y0] x y ⤜
       (λs. BIT_step s x ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) x a))))) = 0"
using assms apply(auto)
  apply(simp_all add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_0y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type0 [x0, y0] x y ⤜
       (λs. BIT_step s y ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) y a))))) = 1"
using assms apply(auto)
  apply(simp_all add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_1x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type1 [x0, y0] x y ⤜
       (λs. BIT_step s x ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) x a))))) = 1/4"
using assms apply(auto)
  apply(simp_all add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_1y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type1 [x0, y0] x y ⤜
       (λs. BIT_step s y ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) y a))))) = 3/4"
using assms apply(auto)
  apply(simp_all add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done
  
lemma costBIT_3x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type3 [x0, y0] x y ⤜
       (λs. BIT_step s x ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) x a))))) = 3/4"
using assms apply(auto)
  apply(simp_all add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_3y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type3 [x0, y0] x y ⤜
       (λs. BIT_step s y ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) y a))))) = 1/4"
using assms apply(auto)
  apply(simp_all add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_4x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type4 [x0, y0] x y ⤜
       (λs. BIT_step s x ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) x a))))) = 0.5"
using assms apply(auto)
  apply(simp_all add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemma costBIT_4y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows
  "E (type4 [x0, y0] x y ⤜
       (λs. BIT_step s y ⤜
            (λ(a, is'). return_pmf (real (tp (fst s) y a))))) = 0.5"
using assms apply(auto)
  apply(simp_all add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf )
  apply(simp_all add: E_bernoulli3 tp_def)
  done

lemmas costBIT = costBIT_0x costBIT_0y costBIT_1x costBIT_1y costBIT_3x costBIT_3y costBIT_4x costBIT_4y

subsubsection "state transformation of BIT"

abbreviation "BIT_Step s x == (s ⤜ (λs. BIT_step s x ⤜ (λ(a, is'). return_pmf (step (fst s) x a, is'))))"

lemma oneBIT_step0x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type0 [x0, y0] x y) x = type0 [x0, y0] x y"
  using assms
  apply(simp add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)   
    done 

lemma oneBIT_step0y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type0 [x0, y0] x y) y = type4 [x0, y0] x y"
  using assms
  apply(simp add: type0_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type4_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type4_def)   
    done 

lemma oneBIT_step1x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type1 [x0, y0] x y) x = type0 [x0, y0] x y"
  using assms
  apply(simp add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)   
    done 

lemma oneBIT_step1y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type1 [x0, y0] x y) y = type3 [x0, y0] x y"
  using assms
  apply(simp add: type1_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type3_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type3_def)   
    done 

lemma oneBIT_step3x: 
    assumes "x≠y" "x:{x0,y0}" "y:{x0,y0}"
    shows "BIT_Step (type3 [x0, y0] x y) x = type1 [x0, y0] x y"
  using assms
  apply(simp add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type1_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type1_def)   
    done

lemma oneBIT_step3y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type3 [x0, y0] x y) y = type0 [x0, y0] y x"
  using assms
  apply(simp add: type3_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)   
    done 

lemma oneBIT_step4x: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type4 [x0, y0] x y) x =  type1 [x0, y0] x y"
  using assms
  apply(simp add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type1_def)
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type1_def)   
    done 

lemma oneBIT_step4y: 
    assumes "x≠y" "x : {x0,y0}" "y∈{x0,y0}"
    shows "BIT_Step (type4 [x0, y0] x y) y = type0 [x0, y0] y x"
  using assms
  apply(simp add: type4_def BIT_step_def bind_assoc_pmf bind_return_pmf step_def mtf2_def)
  apply(safe) 
    apply(rule pmf_eqI) apply(simp add: add.commute pmf_bind swap_def type0_def)
    apply(rule pmf_eqI) apply(simp add: pmf_bind swap_def type0_def)   
    done 
       
lemmas oneBIT_step = oneBIT_step0x oneBIT_step0y oneBIT_step1x oneBIT_step1y oneBIT_step3x oneBIT_step3y oneBIT_step4x oneBIT_step4y      
        
subsection "Analysis of the four phase forms"

subsubsection "yx"
 
lemma bit_yx: assumes "x ≠ y" 
      and kas: "init ∈ {[x,y],[y,x]}"
      and "qs ∈ lang (Star(Times (Atom y) (Atom x))) "
   shows "Tp_on_rand' BIT (type1 init x y) (qs@r) = 0.75 * length qs + Tp_on_rand' BIT (type1 init x y) r 
    ∧ config'_rand BIT (type1 init x y) qs  = (type1 init x y)"
proof -
  from assms have "qs ∈ star ({[y]} @@ {[x]})" by (simp)
  from this assms show ?thesis
  proof (induct qs rule: star_induct)
    case (append u v)
    then have uyx: "u = [y,x]" by auto 
     
    have yy: "Tp_on_rand' BIT (type1 init x y)  (v @ r)  = 0.75*length v + Tp_on_rand' BIT (type1 init x y) r  
            ∧ config'_rand BIT  (type1 init x y) v = (type1 init x y)"
        apply(rule append(3)) 
          apply(fact)+
          using append(2,6) by(simp_all)
     
    have s2: "config'_rand BIT  (type1 init x y) [y,x] = (type1 init x y)"
      using kas assms(1) by (auto simp add: oneBIT_step )
                             
    have ta: "Tp_on_rand' BIT (type1 init x y) u = 1.5"
      using kas assms(1)
        by(auto simp add: uyx oneBIT_step costBIT_1y costBIT_3x)                             
       
    have config: "config'_rand BIT  (type1 init x y) (u @ v)
          = type1 init x y" by (simp only: config'_rand_append s2 uyx yy)

    have "Tp_on_rand' BIT (type1 init x y) (u @ (v @ r))  
        = Tp_on_rand' BIT (type1 init x y) u  + Tp_on_rand' BIT ( config'_rand BIT (type1 init x y)  u) (v@r) "
          by (simp only: T_on_rand'_append)
    also have "… =  Tp_on_rand' BIT  (type1 init x y) u + Tp_on_rand' BIT (type1 init x y) (v@r) "
      unfolding uyx by(simp only: s2) 
    also have "… = Tp_on_rand' BIT (type1 init x y) u  + 0.75*length v + Tp_on_rand' BIT (type1 init x y) r "
        by(simp only: yy) 
    also have "… = 2*0.75 + 0.75*length v + Tp_on_rand' BIT (type1 init x y) r " by(simp add: ta) 
    also have "… = 0.75 * (2+length v) + Tp_on_rand' BIT (type1 init x y) r"
      by (simp add: ring_distribs del: add_2_eq_Suc' add_2_eq_Suc)
    also have "… = 0.75 * length (u @ v) + Tp_on_rand' BIT (type1 init x y) r"
      using uyx by simp
    finally show ?case using config by simp 
  qed simp
qed


subsubsection "(yx)*yx"

lemma bit_yxyx: assumes "x ≠ y" and kas: "init ∈ {[x,y],[y,x]}" and
      "qs ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
   shows "Tp_on_rand' BIT (type0 init x y) (qs@r) = 0.75 * length qs + Tp_on_rand' BIT (type1 init x y) r 
    ∧ config'_rand BIT (type0 init x y) qs  = (type1 init x y)"
proof -
  obtain u v where uu: "u ∈ lang (Times (Atom y) (Atom x))"
              and vv: "v ∈ lang (seq[ Star(Times (Atom y) (Atom x))])"
              and qsuv: "qs = u @ v" 
  using assms(3) by (auto simp: conc_def)  

  from uu have uyx: "u = [y,x]" by(auto)

  from qsuv uyx have vqs: "length v = length qs - 2" by auto
  from qsuv uyx  have vqs2: "length v + 2 = length qs" by auto

  have s2: "config'_rand BIT  (type0 init x y) [y,x] = (type1 init x y)"
     using kas assms(1) by(auto simp add: oneBIT_step) 
                            
  have ta: "Tp_on_rand' BIT (type0 init x y) u = 1.5"
    using kas assms(1) by (auto simp add: uyx oneBIT_step costBIT) 
                  
  have tat: "Tp_on_rand' BIT (type1 init x y) (v @ r) =   0.75*length v + Tp_on_rand' BIT (type1 init x y) r
            ∧ config'_rand BIT (type1 init x y) v = (type1 init x y)"
        apply(rule bit_yx)
      apply(fact)+
      using vv by(simp_all)


  have config: "config'_rand BIT (type0 init x y) (u @ v) = type1 init x y"
    by(simp only: config'_rand_append s2 uyx tat)
     
  have "Tp_on_rand' BIT (type0 init x y) (u @ (v @ r)) 
        = Tp_on_rand' BIT (type0 init x y) u + Tp_on_rand' BIT (config'_rand BIT (type0 init x y) u) (v@r)" by (simp only: T_on_rand'_append)
also
  have "… =  Tp_on_rand' BIT (type0 init x y) u + Tp_on_rand' BIT (type1 init x y) (v@r)" by(simp only: uyx s2) 
also
  have "… = Tp_on_rand' BIT (type0 init x y) u + 0.75*length v + Tp_on_rand' BIT (type1 init x y) r" by(simp only: tat) 
also
  have "… = 2*0.75 + 0.75*length v + Tp_on_rand' BIT (type1 init x y) r" by(simp add: ta) 
also
  have "… = 0.75 * (2+length v) + Tp_on_rand' BIT (type1 init x y) r" by (simp add: ring_distribs del: add_2_eq_Suc' add_2_eq_Suc) 
also
  have "… = 0.75 * length (u @ v) + Tp_on_rand' BIT (type1 init x y) r" using uyx by simp
finally
  show ?thesis using qsuv config by simp
qed

  
subsubsection ‹‹x^+..››

lemma BIT_x: assumes "x≠y"
       "init ∈ {[x,y],[y,x]}" "qs ∈ lang (Plus (Atom x) One)"
 shows "Tp_on_rand' BIT (type0 init x y) (qs@r) = Tp_on_rand' BIT (type0 init x y) r 
    ∧ config'_rand BIT  (type0 init x y) qs = (type0 init x y)"
proof - 
  have s: "config'_rand BIT (type0 init x y) qs = type0 init x y"
    using assms by (auto simp add: oneBIT_step)

  have t: "Tp_on_rand' BIT (type0 init x y) qs = 0"
    using assms by (auto simp add: costBIT)

  show ?thesis using s t by(simp add: T_on_rand'_append)
qed
        

subsubsection "Phase Form A"

lemma BIT_a: assumes "x ≠ y"
    " init ∈ {[x,y],[y,x]}"
   "qs ∈ lang (seq [Plus (Atom x) One, Atom y, Atom y])"
  shows "config'_rand BIT (type0 init x y) qs = (type0 init y x)" (is ?C)
    and b: "Tp_on_rand' BIT (type0 init x y) qs = 1.5" (is ?T) 
proof - 
  from assms(3) have alt: "qs = [x,y,y] ∨ qs = [y,y]" apply(simp) by fastforce
  show ?C
    using assms(1,2) alt by (auto simp add: oneBIT_step)
  show ?T
    using assms(1,2) alt by(auto simp add: oneBIT_step costBIT) 
qed
 
lemma bit_a: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" "qs ∈ lang (seq [Plus (Atom x) One, Atom y, Atom y])"
 shows  
    "Tp_on_rand' BIT s qs  ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y]) 
      ∧  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]
      ∧ Tp_on_rand' BIT s qs = 1.5"
proof -
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have p: "Tp_on_rand' BIT s qs = 1.5"
    unfolding s 
    apply(safe)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done
  with OPT2_A[OF assms(1,5)] have BIT: "Tp_on_rand' BIT s qs ≤ 1.75 * Tp [x, y] qs (OPT2 qs [x, y])" by auto


  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s 
    apply(safe)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule BIT_a)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done 
   
  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def) 

  then show ?thesis using BIT s p by simp
qed  

lemma bit_a'': " a ≠ b ⟹
         {a, b} = {x, y} ⟹
         BIT_inv s a [x, y] ⟹
         set qs ⊆ {a, b} ⟹
         qs ∈ lang (seq [question (Atom a), Atom b, Atom b]) ⟹
         BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] ∧ Tp_on_rand' BIT s qs = 1.5"
using bit_a[of a b x y] by blast


subsubsection "Phase Form B"

lemma BIT_b: assumes A: "x ≠ y"
       "init ∈ {[x,y],[y,x]}"
    "v ∈ lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
    shows "Tp_on_rand' BIT (type0 init x y) v = 0.75 * length v - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init y x)" (is ?C)
proof -
  have lenvmod: "length v mod 2 = 0"
  proof -
    from assms(3) have "v ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by(simp add: conc_assoc)
    then obtain p q r where pqr: "v=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[y]} @@ {[y]}" by (metis concE)
    then have "p = [y,x]" "r=[y,y]" by auto
    with pqr have a: "length v = 4+length q" by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b show "length v mod 2 = 0" by auto
  qed
 
  from assms(3) have "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom y, Atom y])" by (auto simp: conc_def)
  then obtain a b where aa: "a ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b ∈ lang (seq[Atom y, Atom y])"
                      and vab: "v = a @ b" 
                      by(erule concE) 
  then have bb: "b=[y,y]" by auto 
  from vab bb have lenv: "length v = length a + 2" by auto
 
  from bit_yxyx[OF assms(1,2) aa] have stars: "Tp_on_rand' BIT (type0 init x y) (a @ b)  = 0.75 * length a + Tp_on_rand' BIT (type1 init x y) b"
                             and s2: "config'_rand BIT (type0 init x y) a = type1 init x y"  by fast+

  have t: "Tp_on_rand' BIT (type1 init x y) b = 1"
    using assms(1,2) by (auto simp add: oneBIT_step  costBIT bb)   

  have s: "config'_rand BIT  (type1 init x y) [y, y] = type0 init y x" 
    using assms(1,2) by (auto simp add: oneBIT_step) 

  have config: "config'_rand BIT (type0 init x y) (a @ b) = type0 init y x"
    by (simp only: config'_rand_append s2 vab bb s)
 
  have calc: "3 * Suc (Suc (length a)) / 4 - 1 / 2 = 3 * (2+length a) / 4 - 1 / 2" by simp

  from t stars have "Tp_on_rand' BIT (type0 init x y) (a @ b) = 0.75 * length a + 1" by auto
  then show "Tp_on_rand' BIT  (type0 init x y) v = 0.75 * length v - 0.5"
    unfolding lenv by(simp add: vab ring_distribs del: add_2_eq_Suc')
  from config vab show ?C by simp
qed


lemma bit_b''1: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
          Tp_on_rand' BIT s qs  = 0.75 * length qs - 0.5"
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs = 0.75 * length qs - 0.5"
    unfolding s 
    apply(safe)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s 
    apply(safe)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done 
   
  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def) 

  show ?thesis using BIT config by simp
qed


lemma BIT_b2: assumes A: "x ≠ y"
       "init ∈ {[x,y],[y,x]}"
    "v ∈ lang (seq [Atom x, Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
    shows "Tp_on_rand' BIT (type0 init x y) v = 0.75 * (length v - 1) - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init y x)" (is ?C)
proof - 
  from assms(3) obtain w where  vw: "v = [x]@w" and
          w: "w ∈ lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
          by(auto)          
  have c1: "config'_rand BIT (type0 init x y) [x] = type0 init x y"
      using assms by(auto simp add: oneBIT_step)
  have t1: "Tp_on_rand' BIT (type0 init x y) [x] = 0"
      using assms by(auto simp add: costBIT)
  show "Tp_on_rand' BIT (type0 init x y) v
      = 0.75 * (length v - 1) - 0.5"
      unfolding vw apply(simp only: T_on_rand'_append c1 BIT_b[OF assms(1,2) w] t1)
        by (simp)
  show "config'_rand BIT (type0 init x y) v = (type0 init y x)"
    unfolding vw by(simp only: config'_rand_append c1 BIT_b[OF assms(1,2) w])
qed

lemma bit_b''2: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
          Tp_on_rand' BIT s qs  = 0.75 * (length qs - 1) - 0.5"
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs = 0.75 * (length qs-1) - 0.5"
    unfolding s 
    apply(safe)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s 
    apply(safe)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_b2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done 
   
  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def) 

  show ?thesis using BIT config by simp
qed

lemma bit_b: assumes "x ≠ y"
      "init ∈ {[x,y],[y,x]}"
   "qs ∈ lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows  "Tp_on_rand' BIT (type0 init x y) qs ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y])"
  and "config'_rand BIT (type0 init x y) qs = type0 init y x"
proof - 
  obtain u v where uu: "u ∈ lang (Plus (Atom x) One)"
        and vv: "v ∈ lang (seq[Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom y, Atom y])"
        and qsuv: "qs = u @ v" 
        using assms
        by (auto simp: conc_def) 
  have lenv: "length v mod 2 = 0 ∧ last v = y ∧ v≠[]"
  proof -
    from vv have "v ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by simp
    then obtain p q r where pqr: "v=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[y]} @@ {[y]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[y,y]" by auto
    with pqr have a: "length v = 4+length q" by auto

    have "last v = last r" using pqr rr by auto
    then have c: "last v = y" using rr by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b c show ?thesis by auto
  qed
        
  from vv have "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom y, Atom y])" by (auto simp: conc_def)
  then obtain a b where aa: "a ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                    and "b ∈ lang (seq[Atom y, Atom y])"
                    and vab: "v = a @ b" 
                      by(erule concE)  

  from BIT_x[OF assms(1,2) uu] have u_t: "Tp_on_rand' BIT (type0 init x y) (u @ v)  = Tp_on_rand' BIT (type0 init x y) v"
      and u_c: "config'_rand BIT (type0 init x y) u = type0 init x y" by auto
  from BIT_b[OF assms(1,2) vv] have b_t: "Tp_on_rand' BIT (type0 init x y) v  = 0.75 * length v - 0.5"
      and  b_c: "config'_rand BIT (type0 init x y) v = (type0 init y x)" by auto
 
  have BIT: "Tp_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5"
    by(simp add: qsuv u_t b_t)
          
  (* OPT *)

  from uu have uuu: "u=[] ∨ u=[x]" by auto
  have OPT: "Tp [x,y] qs (OPT2 qs [x,y]) = (length v) div 2" apply(rule OPT2_B) by(fact)+

  from lenv have "v ≠ []"  "last v = y" by auto
  then have 1:  "last qs = y" using last_appendR qsuv by simp 
  then have 2: "other (last qs) x y = x" unfolding other_def by simp

  show "Tp_on_rand' BIT (type0 init x y) qs ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y])"
    using BIT OPT lenv by auto

  (* config *)

  show "config'_rand BIT (type0 init x y) qs = type0 init y x"
    by (auto simp add: config'_rand_append qsuv u_c b_c)
qed



lemma bit_b'': assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
 shows  
    "Tp_on_rand' BIT s qs  ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y]) 
      ∧  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]" 
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = y" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs ≤ 1.75 * Tp [x, y] qs (OPT2 qs [x, y])"
    unfolding s 
    apply(safe)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done 

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] y x"
    unfolding s 
    apply(safe)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_b)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done 
   
  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def) 

  then show ?thesis using BIT s by simp
qed

lemma bit_b''': " a ≠ b ⟹
         {a, b} = {x, y} ⟹
         BIT_inv s a [x, y] ⟹
         set qs ⊆ {a, b} ⟹
         qs ∈ lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y]) ⟹
         BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y] ∧ Tp_on_rand' BIT s qs = 1.5"
using bit_a[of a b x y] oops

subsubsection "Phase Form C"

lemma BIT_c: assumes "x ≠ y"
       "init ∈ {[x,y],[y,x]}"
    "v ∈ lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
    shows "Tp_on_rand' BIT (type0 init x y) v = 0.75 * length v - 0.5"
      and "config'_rand BIT  (type0 init x y) v = (type0 init x y)" (is ?C)
proof -        
  have A: "x≠y"  using assms by auto
 
  from assms(3) have "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom x])" by (auto simp: conc_def)
  then obtain a b where aa: "a ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b ∈ lang (seq[Atom x])"
                      and vab: "v = a @ b" 
                      by(erule concE) 
  then have bb: "b=[x]" by auto
  from aa have lena: "length a > 0" by auto
  from vab bb have lenv: "length v = length a + 1" by auto
 
  from bit_yxyx assms(1,2) aa have stars: "Tp_on_rand' BIT (type0 init x y) (a @ b)  = 0.75 * length a + Tp_on_rand' BIT (type1 init x y) b"
                             and s2: "config'_rand BIT (type0 init x y) a = type1 init x y"  by fast+

  have t: "Tp_on_rand' BIT (type1 init x y) b = 1/4"
    using assms(1,2) by (auto simp add: bb costBIT)  
 

  have s: "config'_rand BIT  (type1 init x y) b = type0 init x y" 
    using assms(1,2) by (auto simp add: bb oneBIT_step1x )    


  have config: "config'_rand BIT  (type0 init x y) (a @ b) = type0 init x y"
    by (simp only: config'_rand_append s2 vab s)
 
  have calc: "3 * Suc (Suc (length a)) / 4 - 1 / 2 = 3 * (2+length a) / 4 - 1 / 2" by simp

  from t stars have "Tp_on_rand' BIT (type0 init x y) (a @ b) = 0.75 * length a + 1/4" by auto
  then show "Tp_on_rand' BIT  (type0 init x y) v = 0.75 * length v - 0.5" unfolding lenv 
    by(simp add: vab ring_distribs del: add_2_eq_Suc')
  from config vab show ?C by simp
qed

lemma bit_c''1: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
          Tp_on_rand' BIT s qs  = 0.75 * length qs - 0.5"
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs = 0.75 * length qs - 0.5"
    unfolding s 
    apply(safe) 
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s 
    apply(safe)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done 
   
  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def) 

  show ?thesis using BIT config by simp
qed
           
lemma bit_c: assumes "x ≠ y"
      "init ∈ {[x,y],[y,x]}"
   "qs ∈ lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows  "Tp_on_rand' BIT (type0 init x y) qs ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y])"
  and "config'_rand BIT (type0 init x y) qs = type0 init x y"
proof -
  obtain u v where uu: "u ∈ lang (Plus (Atom x) One)"
        and vv: "v ∈ lang (seq[Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
        and qsuv: "qs = u @ v" 
        using assms
        by (auto simp: conc_def) 
  have lenv: "length v mod 2 = 1 ∧ length v ≥ 3 ∧ last v = x"
  proof -
    from vv have "v ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[x]}" by auto
    then obtain p q r where pqr: "v=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈ {[x]}" by (metis concE)
    then have rr: "p = [y,x]"  "r=[x]" by auto
    with pqr have a: "length v = 3+length q" by auto

    have "last v = last r" using pqr rr by auto
    then have c: "last v = x" using rr by auto

    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b c show "length v mod 2 = 1 ∧ length v ≥ 3 ∧ last v = x" by auto
  qed
        
  from vv have "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])
                          @@ lang (seq[Atom x])" by (auto simp: conc_def)
  then obtain a b where aa: "a ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x))])"
                      and "b ∈ lang (seq[Atom x])"
                      and vab: "v = a @ b" 
                      by(erule concE)  

  from BIT_x[OF assms(1,2) uu] have u_t: "Tp_on_rand' BIT (type0 init x y)  (u @ v)  = Tp_on_rand' BIT (type0 init x y) v"
      and u_c: "config'_rand BIT (type0 init x y) u = type0 init x y" by auto
  from BIT_c[OF assms(1,2) vv] have b_t: "Tp_on_rand' BIT (type0 init x y) v  = 0.75 * length v - 0.5"
      and  b_c: "config'_rand BIT (type0 init x y) v = (type0 init x y)" by auto
 
  have BIT: "Tp_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5"
    by(simp add: qsuv u_t b_t)
          
  (* OPT *)

  from uu have uuu: "u=[] ∨ u=[x]" by auto
  from vv have vvv: "v ∈ lang (seq
          [Atom y, Atom x,
           Star (Times (Atom y) (Atom x)),
           Atom x])" by(auto simp: conc_def)
  have OPT: "Tp [x,y] qs (OPT2 qs [x,y]) = (length v) div 2" apply(rule OPT2_C) by(fact)+


  from lenv have "v ≠ []"  "last v = x" by auto
  then have 1:  "last qs = x" using last_appendR qsuv by simp 
  then have 2: "other (last qs) x y = y" unfolding other_def by simp



  have vgt3: "length v ≥ 3" using lenv by simp
  have "Tp_on_rand' BIT (type0 init x y) qs  = 0.75 * length v - 0.5" using BIT by simp
also
  have "… ≤ 1.75 * (length v - 1)/2"
  proof -
    have "10 + 6 * length v ≤ 7 * Suc (length v) 
        ⟷ 10 + 6 * length v ≤ 7 * length v + 7" by auto
    also have "… ⟷ 3 ≤ length v" by auto
    also have "… ⟷ True" using vgt3 by auto
    finally have A: " 6 * length v - 4 ≤ 7 * (length v - 1)" by simp
    show ?thesis apply(simp) using A by linarith 
  qed    
also
  have "… = 1.75 * (length v div 2)"
  proof -
    from div_mult_mod_eq have "length v = length v div 2 * 2 + length v mod 2" by auto
    with lenv have "length v = length v div 2 * 2 + 1" by auto 
    then have "(length v - 1) / 2 = length v div 2" by simp
    then show ?thesis by simp
  qed
also
  have "… = 1.75 * Tp [x, y] qs (OPT2 qs [x, y])" using OPT by auto
finally
  show "Tp_on_rand' BIT (type0 init x y) qs ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y])"
    using BIT OPT lenv   1 2  by auto

  (* config *)

  show "config'_rand BIT  (type0 init x y) qs  = type0 init x y"
    by (auto simp add: config'_rand_append qsuv u_c b_c)
qed

lemma bit_c'': assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Plus (Atom x) One, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows  
    "Tp_on_rand' BIT s qs  ≤ 1.75 * Tp [x,y] qs (OPT2 qs [x,y]) 
      ∧  BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]" 
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs ≤ 1.75 * Tp [x, y] qs (OPT2 qs [x, y])"
    unfolding s 
    apply(safe)
      apply(rule bit_c )
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done 

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s 
    apply(safe)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
      apply(rule bit_c)
        apply(simp) apply(simp) using assms(5) apply(simp)
  done 
   
  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def) 

  then show ?thesis using BIT s by simp
qed  




lemma BIT_c2: assumes A: "x ≠ y"
       "init ∈ {[x,y],[y,x]}"
    "v ∈ lang (seq [Atom x, Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
    shows "Tp_on_rand' BIT (type0 init x y) v = 0.75 * (length v - 1) - 0.5" (is ?T)
     and "config'_rand BIT  (type0 init x y) v = (type0 init x y)" (is ?C)
proof - 
  from assms(3) obtain w where  vw: "v = [x]@w" and
          w: "w ∈ lang (seq [Times (Atom y) (Atom x), Star (Times (Atom y) (Atom x)), Atom x])"
          by(auto)          
  have c1: "config'_rand BIT (type0 init x y) [x] = type0 init x y"
      using assms by(auto simp add: oneBIT_step)
  have t1: "Tp_on_rand' BIT (type0 init x y) [x] = 0"
      using assms by(auto simp add: costBIT)
  show "Tp_on_rand' BIT (type0 init x y) v
      = 0.75 * (length v - 1) - 0.5"
      unfolding vw apply(simp only: T_on_rand'_append c1 BIT_c[OF assms(1,2) w] t1)
        by (simp)
  show "config'_rand BIT (type0 init x y) v = (type0 init x y)"
    unfolding vw by(simp only: config'_rand_append c1 BIT_c[OF assms(1,2) w])
qed

lemma bit_c''2: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" 
    "qs ∈ lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
 shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
          Tp_on_rand' BIT s qs  = 0.75 * (length qs - 1) - 0.5"
proof -  
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast

  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto

  from assms(5) have lqs: "last qs = x" by fastforce
  from assms(1,2) kas have BIT: "Tp_on_rand' BIT s qs = 0.75 * (length qs-1) - 0.5"
    unfolding s 
    apply(safe)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done

  from assms(1,2) kas have "config'_rand BIT s qs = type0 [x0, y0] x y"
    unfolding s 
    apply(safe)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
      apply(rule BIT_c2)
        apply(simp) apply(simp) using assms(5) apply(simp add: conc_assoc)
  done 
   
  then have config: "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas lqs by(auto simp add: BIT_inv2 other_def) 

  show ?thesis using BIT config by simp
qed


subsubsection "Phase Form D"
 
lemma bit_d: assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" "qs ∈ lang (seq [Atom x, Atom x])"
  shows "Tp_on_rand' BIT s qs ≤ 175 / 102 * real (Tp [x, y] qs (OPT2 qs [x, y])) ∧
    BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
     Tp_on_rand' BIT s qs = 0"
proof - 
  from assms have qs: "qs = [x,x]" by auto
  then have OPT: "Tp [x, y] qs (OPT2 qs [x, y]) = 0" by (simp add: tp_def step_def)
   
  from assms have f: "x0≠y0" by auto
  from assms(1,3) assms(2)[symmetric] have s: "s = type0 [x0,y0] x y"
    apply(simp add: BIT_inv2[OF f] other_def) by fast
    
  from assms(1,2) have kas: "[x,y] = [x0,y0] ∨ [x,y] = [y0,x0]" by auto
 
  have BIT: "Tp_on_rand' BIT (type0 [x0,y0] x y) qs = 0"
    using kas assms(1,2) by (auto simp add: qs oneBIT_step costBIT) 

  have lqs: "last qs = x" "last qs ∈ {x0,y0}" using assms(2,4) qs by auto 

  have inv: "config'_rand BIT s qs = type0 [x0, y0] x y"
    using kas assms(1,2) by (auto simp add: qs s  oneBIT_step0x) 
   
  then have "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0]"
    apply(simp)
    using assms(1) kas f lqs by(auto simp add: BIT_inv2 other_def) 
    
  then show ?thesis using BIT s by(auto)
qed

lemma bit_d': assumes 
    "x ≠ y" "{x, y} = {x0, y0}" "BIT_inv s x [x0, y0]"
    "set qs ⊆ {x, y}" "qs ∈ lang (seq [Atom x, Atom x])"
  shows "BIT_inv (config'_rand BIT s qs) (last qs) [x0, y0] ∧
     Tp_on_rand' BIT s qs = 0"
using bit_d[OF assms] by blast



subsection "Phase Partitioning"

lemma BIT_inv_initial: assumes "(x::nat) ≠ y"
    shows "BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y]"
using assms(1) apply(simp add: BIT_inv2 BIT_init_def type0_def)
      apply(simp add: map_pmf_def other_def bind_return_pmf bind_assoc_pmf)
      using bind_commute_pmf by fast

lemma D'': assumes "qs ∈ Lxx a b"
    "a ≠ b" "{a, b} = {x, y}" "BIT_inv s a [x, y]"
    "set qs ⊆ {a, b}"
 shows "Tp_on_rand' BIT s qs ≤ 175 / 102 * real (Tp [a, b] qs (OPT2 qs [a, b])) ∧
    BIT_inv (Partial_Cost_Model.config'_rand BIT s qs) (last qs) [x, y]"
 apply(rule LxxE[OF assms(1)])
  using bit_d[OF assms(2-5)] apply(simp)
  apply(rule bit_b''[OF assms(2-5)]) apply(simp)
  apply(rule bit_c''[OF assms(2-5)]) apply(simp) 
  using bit_a[OF assms(2-5)] apply(simp)
  done

theorem BIT_175comp_on_2:
    assumes "(x::nat) ≠ y" "set σ ⊆ {x,y}"     
     shows "Tp_on_rand BIT [x,y] σ  ≤ 1.75 * real (Tp_opt [x,y] σ) + 1.75" 
proof (rule Phase_partitioning_general[where P=BIT_inv], goal_cases)
  case 4
  show "BIT_inv (map_pmf (Pair [x, y]) (fst BIT [x, y])) x [x, y]"
   by (rule BIT_inv_initial[OF assms(1)])
next
  case (5 a b qs s)
  then show ?case by(rule D'')
qed (simp_all add: assms)  
 
end