Theory EdmondsKarp_Time

theory EdmondsKarp_Time
  imports EdmondsKarp_Impl 
begin
 
lemma "(λx::nat. real ((3 ))) ∈ Θ(λ(x). real 1)" 
  by auto2 

lemma "(λx. real ((32 ))) ∈ Θ⇩2(λ(V::nat,E::nat). 1)"
  apply (subst surjective_pairing) by auto2

lemma "(λx. real ((rbt_insert_logN 1 ))) ∈ Θ⇩2(λ(V::nat,E::nat). 1)" 
  apply (subst surjective_pairing) by auto2

lemma edka_runt: "edka_cost ∈ Θ⇩2(λ(V::nat,E::nat). V * E * V + V * E * E  )"
  apply (subst surjective_pairing)
  unfolding edka_cost_simp by auto2


lemma final_running_time: "edka_cost ∈ Θ⇩2(λ(V::nat,E::nat). (V * E) * (V + E) )"
proof -
  have *:  "⋀E V::nat. (V * E) * (V + E) = V * E * V + V * E * E"  
    by (simp add: distrib_left)  
  show ?thesis unfolding * using edka_runt  
    by simp
qed 

end