Theory IFC

section ‹Definitions›

text ‹
This section contains all necessary definitions of this development. Section~\ref{sec:pm} contains 
the structural definition of our program model which includes the security specification as well 
as abstractions of control flow and data.  Executions of our program model are defined in 
section~\ref{sec:ex}.  Additional well-formedness properties are defined in section~\ref{sec:wf}. 
Our security property is defined in section~\ref{sec:sec}.  Our characterisation of how information
is propagated by executions of our program model is defined in section~\ref{sec:char-cp}, for which
the correctness result can be found in section~\ref{sec:cor-cp}.  Section~\ref{sec:char-scp} contains
an additional approximation of this characterisation whose correctness result can be found in 
section~\ref{sec:cor-scp}.
›


theory IFC
  imports Main
begin

subsection ‹Program Model›
text_raw ‹\label{sec:pm}›

text ‹Our program model contains all necessary components for the remaining development and consists of:›

record ('n, 'var, 'val, 'obs) ifc_problem =  
― ‹A set of nodes representing program locations:›
  nodes :: 'n set
― ‹An initial node where all executions start:›
  entry :: 'n
― ‹A final node where executions can terminate:›
  return :: 'n
― ‹An abstraction of control flow in the form of an edge relation:›
  edges :: ('n × 'n) set
― ‹An abstraction of variables written at program locations:›
  writes :: 'n  'var set
― ‹An abstraction of variables read at program locations:›
  reads :: 'n  'var set
― ‹A set of variables containing the confidential information in the initial state:›
  hvars :: 'var set
― ‹A step function on location state pairs:›
  step :: ('n × ('var  'val))  ('n × ('var  'val))
― ‹An attacker model producing observations based on the reached state at certain locations:›
  att :: 'n  (('var  'val)  'obs)

text ‹We fix a program in the following in order to define the central concepts.  
The necessary well-formedness assumptions will be made in section~\ref{sec:wf}.›
locale IFC_def =
fixes prob :: ('n, 'var, 'val, 'obs) ifc_problem
begin  

text ‹Some short hands to the components of the program which we will utilise exclusively in the following.›
definition nodes where nodes = ifc_problem.nodes prob
definition entry where entry = ifc_problem.entry prob
definition return where return = ifc_problem.return prob
definition edges where edges = ifc_problem.edges prob
definition writes where writes = ifc_problem.writes prob
definition reads where reads = ifc_problem.reads prob
definition hvars where hvars = ifc_problem.hvars prob
definition step where step = ifc_problem.step prob
definition att where att = ifc_problem.att prob

text ‹The components of the step function for convenience.›
definition suc where suc n σ = fst (step (n, σ))
definition sem where sem n σ = snd (step (n, σ))

lemma step_suc_sem: step (n,σ) = (suc n σ, sem n σ) unfolding suc_def sem_def by auto


subsubsection ‹Executions›
text ‹\label{sec:ex}›
text ‹In order to define what it means for a program to be well-formed, we first require concepts 
of executions and program paths.›

text ‹The sequence of nodes visited by the execution corresponding to an input state.›
definition path where
path σ k= fst ((step^^k) (entry,σ))

text ‹The sequence of states visited by the execution corresponding to an input state.›
definition kth_state ( ‹__ [111,111] 110) where 
σk= snd ((step^^k) (entry,σ))

text ‹A predicate asserting that a sequence of nodes is a valid program path according to the
control flow graph.›

definition is_path where
is_path π = ( n. (π n, π (Suc n))  edges) 
end

subsubsection ‹Well-formed Programs›
text_raw ‹\label{sec:wf}›

text ‹The following assumptions define our notion of valid programs.›
locale IFC = IFC_def prob for prob:: ('n, 'var, 'val, 'out) ifc_problem +
assumes ret_is_node[simp,intro]: return  nodes
and entry_is_node[simp,intro]: entry  nodes
and writes:  v n. (σ. σ v  sem n σ v)  v  writes n
and writes_return: writes return = {}
and uses_writes:  n σ σ'. ( v  reads n. σ v = σ' v)   v  writes n. sem n σ v = sem n σ' v
and uses_suc:  n σ σ'. ( v  reads n. σ v = σ' v)  suc n σ = suc n σ'
and uses_att:  n f σ σ'. att n = Some f  ( v  reads n. σ v = σ' v)  f σ = f σ'
and edges_complete[intro,simp]: m σ. m  nodes  (m,suc m σ)  edges
and edges_return : x. (return,x)  edges  x = return
and edges_nodes: edges  nodes × nodes    
and reaching_ret:  x. x  nodes   π n. is_path π  π 0 = x  π n = return


subsection ‹Security›
text_raw ‹\label{sec:sec}›

text ‹We define our notion of security, which corresponds to what Bohannon et al.~cite"Bohannon:2009:RN:1653662.1653673" 
refer to as indistinguishable security.  In order to do so we require notions of observations made
by the attacker, termination and equivalence of input states.›

context IFC_def
begin

subsubsection ‹Observations›
text_raw ‹\label{sec:obs}›

text ‹The observation made at a given index within an execution.›
definition obsp where
obsp σ k = (case att(path σ k) of Some f  Some (f (σk)) | None  None)

text ‹The indices within a path where an observation is made.›
definition obs_ids :: (nat  'n)  nat set where
obs_ids π = {k. att (π k)  None}

text ‹A predicate relating an observable index to the number of observations made before.›
definition is_kth_obs :: (nat  'n)  nat  nat  boolwhere
is_kth_obs π k i = (card (obs_ids π  {..<i}) = k  att (π i)   None)

text ‹The final sequence of observations made for an execution.›
definition obs where
obs σ k = (if (i. is_kth_obs (path σ) k i) then obsp σ (THE i. is_kth_obs (path σ) k i) else None)

text ‹Comparability of observations.›
definition obs_prefix :: (nat  'obs option)  (nat  'obs option)  bool (infix  50) where
a  b   i. a i  None  a i = b i

definition obs_comp (infix  50) where
a  b  a  b  b  a

subsubsection ‹Low equivalence of input states›

definition restrict (infix  100 ) where
fU = (λ n. if n  U then f n else undefined)

text ‹Two input states are low equivalent if they coincide on the non high variables.›
definition loweq (infix =L 50) 
where σ =L σ' = (σ(-hvars) = σ'(-hvars))

subsubsection ‹Termination›

text ‹An execution terminates iff it reaches the terminal node at any point.›
definition terminates where
terminates σ   i. path σ i = return


subsubsection ‹Security Property›
text ‹The fixed program is secure if and only if for all pairs of low equivalent inputs the observation
sequences are comparable and if the execution for an input state terminates then the observation sequence 
is not missing any observations.›

definition secure where
secure   σ σ'. σ =L σ'  (obs σ  obs σ'  (terminates σ  obs σ'  obs σ))



subsection ‹Characterisation of Information Flows›
text ‹We now define our characterisation of information flows which tracks data and control dependencies 
within executions. To do so we first require some additional concepts.›

subsubsection ‹Post Dominance›
text ‹We utilise the post dominance relation in order to define control dependence.›

text ‹The basic post dominance relation.›
definition is_pd (infix pd→ 50) where 
y pd→ x  x  nodes  ( π n. is_path π  π (0::nat) = x  π n = return  (kn. π k = y))

text ‹The immediate post dominance relation.›
definition is_ipd (infix ipd→ 50)where
y ipd→ x  x  y  y pd→ x  ( z. zx  z pd→ x  z pd→ y)

definition ipd where 
ipd x = (THE y. y ipd→ x)

text ‹The post dominance tree.›
definition pdt where
pdt = {(x,y). xy  y pd→ x}


subsubsection ‹Control Dependence›

text ‹An index on an execution path is control dependent upon another if the path does not visit
the immediate post domiator of the node reached by the smaller index.›
definition is_cdi (‹_ cd⇗_⇖→ _› [51,51,51]50) where
i cd⇗π⇖→ k  is_path π  k < i  π i  return  ( j  {k..i}. π j  ipd (π k)) 

text ‹The largest control dependency of an index is the immediate control dependency.›
definition is_icdi (‹_ icd⇗_⇖→ _› [51,51,51]50) where
n icd⇗π⇖→ n'  is_path π  n cd⇗π⇖→ n'  ( m  {n'<..<n}.¬ n cd⇗π⇖→ m)

text ‹For the definition of the control slice, which we will define next, we require the uniqueness 
of the immediate control dependency.›

lemma icd_uniq: assumes  m icd⇗π⇖→ n m icd⇗π⇖→ n' shows n = n'
proof - 
  {
    fix n n' assume *: m icd⇗π⇖→ n m icd⇗π⇖→ n' n < n'
    have n'<m using * unfolding is_icdi_def is_cdi_def by auto    
    hence ¬ m cd⇗π⇖→ n' using * unfolding is_icdi_def by auto
    with *(2) have False unfolding is_icdi_def by auto
  }
  thus ?thesis using assms by (metis linorder_neqE_nat)
qed


subsubsection ‹Control Slice›
text ‹We utilise the control slice, that is the sequence of nodes visited by the control dependencies 
of an index, to match indices between executions.›

function cs:: (nat  'n)  nat  'n list (cs⇗_ _› [51,70] 71) where
‹cs⇗πn = (if ( m. n icd⇗π⇖→ m) then (cs π (THE m. n icd⇗π⇖→ m))@[π n] else [π n]) 
by pat_completeness auto  
termination cs proof
  show wf (measure snd) by simp
  fix π n  
  define m where m == (The (is_icdi n π))
  assume Ex (is_icdi n π) 
  hence n icd⇗π⇖→ m unfolding m_def by (metis (full_types) icd_uniq theI')
  hence m < n unfolding is_icdi_def is_cdi_def by simp
  thus ((π, The (is_icdi n π)), π, n)  measure snd by (metis in_measure m_def snd_conv)
qed

inductive cs_less (infix  50) where
length xs < length ys  take (length xs) ys = xs   xs  ys     

definition cs_select (infix ¡ 50) where
π¡xs = (THE k. cs⇗πk = xs)


subsubsection ‹Data Dependence›

text ‹Data dependence is defined straight forward. An index is data dependent upon another, 
if the index reads a variable written by the earlier index and the variable in question has not 
been written by any index in between.›
definition is_ddi (‹_ dd⇗_,_⇖→ _› [51,51,51,51] 50) where
n dd⇗π,v⇖→ m  is_path π  m < n  v  reads (π n)  (writes (π m))  ( l  {m<..<n}. v  writes (π l))



subsubsection ‹Characterisation via Critical Paths›
text_raw ‹\label{sec:char-cp}›
text ‹With the above we define the set of critical paths which as we will prove characterise the matching
points in executions where diverging data is read.›

inductive_set cp where

― ‹Any pair of low equivalent input states and indices where a diverging high variable is first
read is critical.›

σ =L σ'; 
  cs⇗path σn = cs⇗path σ'n'; 
  h  reads(path σ n); 
  (σn) h  (σ'n') h; 
   k<n. hwrites(path σ k); 
   k'<n'. hwrites(path σ' k')
   ((σ,n),(σ',n'))  cp |

― ‹If from a pair of critical indices in two executions there exist data dependencies from both
indices to a pair of matching indices where the variable diverges, the later pair of indices is critical.›

((σ,k),(σ',k'))  cp; 
  n dd⇗path σ,v⇖→ k;
  n' dd⇗path σ',v⇖→ k'; 
  cs⇗path σn = cs⇗path σ'n'; 
  (σn) v  (σ'n') v
   ((σ,n),(σ',n'))  cp |

― ‹If from a pair of critical indices the executions take different branches and one of the critical 
indices is a control dependency of an index that is data dependency of a matched index where diverging 
data is read and the variable in question is not written by the other execution after the executions
first reached matching indices again, then the later matching pair of indices is critical.›

((σ,k),(σ',k'))  cp; 
  n dd⇗path σ,v⇖→ l; 
  l cd⇗path σ⇖→ k; 
  cs⇗path σn = cs⇗path σ'n'; 
  path σ (Suc k)  path σ' (Suc k'); 
  (σn) v  (σ'n') v; 
  j'{(LEAST i'. k' < i'  (i. cs⇗path σi = cs⇗path σ'i'))..<n'}. vwrites (path σ' j')
   ((σ,n),(σ',n'))  cp | 

― ‹The relation is symmetric.›

((σ,k),(σ',k'))  cp  ((σ',k'),(σ,k))  cp


text ‹Based on the set of critical paths, the critical observable paths are those that either directly 
reach observable nodes or are diverging control dependencies of an observable index.›

inductive_set cop where
((σ,n),(σ',n'))  cp;
  path σ n  dom att
   ((σ,n),(σ',n'))  cop |

((σ,k),(σ',k'))  cp; 
  n cd⇗path σ⇖→ k; 
  path σ (Suc k)  path σ' (Suc k'); 
  path σ n  dom att
   ((σ,n),(σ',k'))  cop



subsubsection ‹Approximation via Single Critical Paths›
text_raw ‹\label{sec:char-scp}›

text ‹For applications we also define a single execution approximation.›

definition is_dcdi_via (‹_ dcd⇗_,_⇖→ _ via _ _› [51,51,51,51,51,51] 50) where
n dcd⇗π,v⇖→ m via π' m' = (is_path π  m < n  ( l' n'. cs⇗πm = cs⇗π'm'  cs⇗πn = cs⇗π'n'  n' dd⇗π',v⇖→ l'  l' cd⇗π'⇖→ m')  ( l  {m..<n}. v writes(π l)))

inductive_set scp where
h  hvars; h  reads (path σ n); ( k<n. h writes(path σ k))  (path σ,n)  scp |
(π,m)  scp; n cd⇗π⇖→ m  (π,n)  scp|
(π,m)  scp; n dd⇗π,v⇖→ m  (π,n)  scp|
(π,m)  scp; (π',m')  scp; n dcd⇗π,v⇖→ m via π' m'  (π,n)  scp

inductive_set scop where
(π,n)  scp; π n  dom att  (π,n)  scop



subsubsection ‹Further Definitions›
text ‹The following concepts are utilised by the proofs.›

inductive contradicts (infix 𝔠 50) where
cs⇗π'k'  cs⇗πk ; π = path σ;  π' = path σ' ; π (Suc (π¡cs⇗π'k'))  π' (Suc k')  (σ', k') 𝔠 (σ, k)|
cs⇗π'k' = cs⇗πk ; π = path σ;  π' = path σ' ; σk (reads (π k))  σ'k' (reads (π k))  (σ',k') 𝔠 (σ,k)

definition path_shift (infixl « 51) where 
[simp]: π«m = (λ n. π (m+n)) 

definition path_append :: (nat  'n)  nat  (nat  'n)  (nat  'n) (‹_ @⇗_ _› [0,0,999] 51) where
[simp]: π @⇗mπ' = (λn.(if n  m then π n else π' (n-m))) 

definition eq_up_to :: (nat  'n)  nat  (nat  'n)  bool (‹_ =⇘_ _› [55,55,55] 50) where
π =⇘kπ' = ( i  k. π i = π' i)

end (* End of locale IFC_def *)




section ‹Proofs›
text_raw ‹\label{sec:proofs}›

subsection ‹Miscellaneous Facts›

lemma option_neq_cases: assumes x  y obtains (none1) a where x = None y = Some a | (none2) a where x = Some a y = None | (some) a b where x = Some a y = Some b a  b using assms by fastforce

lemmas nat_sym_cases[case_names less sym eq] = linorder_less_wlog

lemma mod_bound_instance: assumes j < (i::nat) obtains j' where k < j' and j' mod i = j  proof -
  have k < Suc k * i + j using assms less_imp_Suc_add by fastforce
  moreover
  have (Suc k * i + j) mod i = j by (metis assms mod_less mod_mult_self3) 
  ultimately show thesis using that by auto
qed

lemma list_neq_prefix_cases: assumes ls  ls' and ls  Nil and ls'  Nil
  obtains (diverge) xs x x' ys ys' where ls = xs@[x]@ys ls' = xs@[x']@ys' x  x' |
   (prefix1) xs where ls = ls'@xs and xs  Nil |
   (prefix2) xs where ls@xs = ls' and xs  Nil 
using assms proof (induct length ls arbitrary: ls ls' rule: less_induct)
  case (less ls ls')
  obtain z zs z' zs' where
  lz: ls = z#zs ls' = z'#zs' by (metis list.exhaust less(6,7))
  show ?case proof cases
    assume zz: z = z'
    hence zsz: zs  zs' using less(5) lz by auto
    have lenz: length zs < length ls using lz by auto    
    show ?case proof(cases zs = Nil)
      assume zs: zs = Nil
      hence zs'  Nil using zsz by auto
      moreover
      have ls@zs' = ls' using zs lz zz by auto
      ultimately
      show thesis using less(4) by blast
    next
      assume zs: zs  Nil
      show thesis proof (cases zs' = Nil)
        assume zs' = Nil
        hence ls = ls'@zs using lz zz by auto
        thus thesis using zs less(3) by blast
      next
        assume zs': zs'  Nil
        { fix xs x ys x' ys' 
          assume zs = xs @ [x] @ ys zs' = xs @ [x'] @ ys' and xx: x  x'
          hence ls = (z#xs) @ [x] @ ys ls' = (z#xs) @ [x'] @ ys' using lz zz by auto
          hence thesis using less(2) xx by blast
        } note * = this
        { fix xs 
          assume zs = zs' @ xs and xs: xs  []
          hence ls = ls' @ xs using lz zz by auto
          hence thesis using xs less(3) by blast
        } note ** = this
        { fix xs 
          assume zs@xs = zs' and xs: xs  []
          hence ls@xs = ls' using lz zz by auto
          hence thesis using xs less(4) by blast
        } note *** = this
        have (xs x ys x' ys'. zs = xs @ [x] @ ys  zs' = xs @ [x'] @ ys'  x  x'  thesis)  
              (xs. zs = zs' @ xs  xs  []  thesis)  
              (xs. zs @ xs = zs'  xs  []  thesis)  thesis 
        using less(1)[OF lenz _ _ _ zsz zs zs' ] .
        thus thesis using * ** *** by blast
      qed
    qed 
  next
    assume z  z'
    moreover
    have ls = []@[z]@zs ls' = []@[z']@zs' using lz by auto
    ultimately show thesis using less(2) by blast
  qed
qed

lemma three_cases: assumes A  B  C obtains A | B | C using assms by auto

lemma insort_greater:  x  set ls. x < y  insort y ls = ls@[y] by (induction ls,auto) 

lemma insort_append_first: assumes  y  set ys. x  y shows insort x (xs@ys) = insort x xs @ ys using assms by (induction xs,auto,metis insort_is_Cons)

lemma sorted_list_of_set_append: assumes finite xs finite ys  x  xs.  y  ys. x < y shows sorted_list_of_set (xs  ys) = sorted_list_of_set xs @ (sorted_list_of_set ys)
using assms(1,3) proof (induction xs)
  case empty thus ?case by simp
next
  case (insert x xs)
  hence iv: sorted_list_of_set (xs  ys) = sorted_list_of_set xs @ sorted_list_of_set ys by blast
  have le:  y  set (sorted_list_of_set ys). x < y using insert(4) assms(2) sorted_list_of_set by auto
  have sorted_list_of_set (insert x xs  ys) = sorted_list_of_set (insert x (xs  ys)) by auto
  also 
  have  = insort x (sorted_list_of_set (xs  ys)) by (metis Un_iff assms(2) finite_Un insert.hyps(1) insert.hyps(2) insert.prems insertI1 less_irrefl sorted_list_of_set_insert)
  also 
  have  = insort x (sorted_list_of_set xs @ sorted_list_of_set ys) using iv by simp
  also
  have  = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys  by (metis le insort_append_first less_le_not_le)
  also 
  have  = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys using sorted_list_of_set_insert[OF insert(1),of x] insert(2) by auto
  finally  
  show ?case .
qed

lemma filter_insort: sorted xs  filter P (insort x xs) = (if P x then insort x (filter P xs) else filter P xs) by (induction xs, simp) (metis filter_insort filter_insort_triv map_ident) 

lemma filter_sorted_list_of_set: assumes finite xs shows filter P (sorted_list_of_set xs) = sorted_list_of_set {x  xs. P x} using assms proof(induction xs)
  case empty thus ?case by simp
next  
  case (insert x xs)
  have *: set (sorted_list_of_set xs) = xs sorted (sorted_list_of_set xs) distinct (sorted_list_of_set xs) by (auto simp add: insert.hyps(1))
  have **: P x  {y  insert x xs. P y} = insert x {y  xs. P y} by auto
  have ***: ¬ P x  {y  insert x xs. P y} = {y  xs. P y} by auto
  note filter_insort[OF *(2),of P x] sorted_list_of_set_insert[OF insert(1), of x] insert(2,3) ** ***  
  thus ?case by (metis (mono_tags) "*"(1) List.finite_set distinct_filter distinct_insort distinct_sorted_list_of_set set_filter sorted_list_of_set_insert)
qed

lemma unbounded_nat_set_infinite: assumes  (i::nat).  ji. j  A shows ¬ finite A using assms
by (metis finite_nat_set_iff_bounded_le not_less_eq_eq)

lemma infinite_ascending: assumes nf: ¬ finite (A::nat set) obtains f where range f = A  i. f i < f (Suc i) proof 
  let ?f = λ i. (LEAST a. a  A  card (A  {..<a}) = i)
  { fix i 
    obtain a where a  A card (A  {..<a}) = i 
    proof (induction i arbitrary: thesis)
      case 0
      let ?a0 = (LEAST a. a  A)
      have ?a0  A by (metis LeastI empty_iff finite.emptyI nf set_eq_iff)      
      moreover
      have b. b  A  ?a0  b by (metis Least_le)
      hence card (A  {..<?a}) = 0 by force
      ultimately
      show ?case using 0 by blast
    next
      case (Suc i)
      obtain a where aa: a  A and card: card (A  {..<a}) = i using Suc.IH by metis
      have nf': ~ finite (A - {..a}) using nf by auto
      let ?b = LEAST b. b  A - {..a}
      have bin: ?b  A-{..a} by (metis LeastI empty_iff finite.emptyI nf' set_eq_iff)
      have le: c. c  A-{..a}  ?b  c by (metis Least_le)
      have ab: a < ?b using bin by auto
      have  c. c  A  c < ?b  c  a using le by force
      hence A  {..<?b} = insert a (A  {..<a}) using bin ab aa by force 
      hence card (A {..<?b}) = Suc i using card by auto
      thus ?case using Suc.prems bin by auto
    qed
    note  thesis. ((a. a  A  card (A  {..<a}) = i  thesis)  thesis)
  }
  note ex = this
    
  {
    fix i
    obtain a where a: a  A  card (A {..<a}) = i  using ex by blast
    have ina: ?f i  A and card: card (A {..<?f i}) = i using LeastI[of λ a. a  A  card (A {..<a}) = i a, OF a] by auto    
    obtain b where b: b  A  card (A {..<b}) = Suc i  using ex by blast
    have inab: ?f (Suc i)  A and cardb: card (A {..<?f (Suc i)}) = Suc i using LeastI[of λ a. a  A  card (A {..<a}) = Suc i b, OF b] by auto
    have ?f i < ?f (Suc i) proof (rule ccontr)
      assume ¬ ?f i < ?f (Suc i)
      hence A {..<?f (Suc i)}  A {..<?f i} by auto
      moreover have finite (A {..<?f i}) by auto
      ultimately have card(A {..<?f (Suc i)})  card (A {..<?f i}) by (metis (erased, lifting) card_mono)
      thus False using card cardb by auto 
    qed
    note this ina
  }
  note b = this
  thus  i. ?f i < ?f (Suc i) by auto
  have *: range ?f  A using b by auto
  moreover
  { 
    fix a assume ina: a  A
    let ?i = card (A  {..<a})
    obtain b where b: b  A  card (A {..<b}) = ?i  using ex by blast
    have inab: ?f ?i  A and cardb: card (A {..<?f ?i}) = ?i using LeastI[of λ a. a  A  card (A {..<a}) = ?i b, OF b] by auto
    have le: ?f ?i  a using Least_le[of λ a. a  A  card (A {..<a}) = ?i a] ina by auto    
    have a = ?f ?i proof (rule ccontr)
      have fin: finite (A  {..<a}) by auto
      assume a  ?f ?i
      hence ?f ?i < a using le by simp
      hence ?f ?i  A  {..<a} using inab by auto
      moreover
      have A  {..<?f ?i}  A  {..<a} using le by auto
      hence A  {..<?f ?i} = A  {..<a} using cardb card_subset_eq[OF fin] by auto
      ultimately      
      show False by auto
    qed
    hence a  range ?f by auto
  }
  hence A  range ?f by auto 
  ultimately show range ?f = A by auto
qed

lemma mono_ge_id:  i. f i < f (Suc i)  i  f i 
  apply (induction i,auto) 
  by (metis not_le not_less_eq_eq order_trans)

lemma insort_map_mono: assumes mono:  n m. n < m  f n < f m shows map f (insort n ns) = insort (f n) (map f ns)
  apply (induction ns)
   apply auto
     apply (metis not_less not_less_iff_gr_or_eq mono)
    apply (metis antisym_conv1 less_imp_le mono)
   apply (metis mono not_less)
  by (metis mono not_less)  

lemma sorted_list_of_set_map_mono: assumes mono:  n m. n < m  f n < f m and fin: finite A
shows map f (sorted_list_of_set A) = sorted_list_of_set (f`A)
using fin proof (induction)
  case empty thus ?case by simp
next
  case (insert x A)
  have [simp]:sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A) using insert sorted_list_of_set_insert by simp
  have f ` insert x A = insert (f x) (f ` A) by auto
  moreover
  have f x  f`A apply (rule ccontr) using insert(2) mono apply auto by (metis insert.hyps(2) mono neq_iff)
  ultimately
  have sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f`A)) using insert(1) sorted_list_of_set_insert by simp
  also
  have  = insort (f x) (map f (sorted_list_of_set A)) using insert.IH by auto
  also have  = map f (insort x (sorted_list_of_set A)) using insort_map_mono[OF mono] by auto
  finally  
  show map f (sorted_list_of_set (insert x A)) = sorted_list_of_set (f ` insert x A) by simp
qed

lemma GreatestIB:
fixes n :: nat and P
assumes a:kn. P k
shows GreatestBI: P (GREATEST k. kn  P k) and GreatestB: (GREATEST k. kn  P k)  n 
proof -
  show P (GREATEST k. kn  P k) using GreatestI_ex_nat[OF assms] by auto  
  show (GREATEST k. kn  P k)  n using GreatestI_ex_nat[OF assms] by auto
qed

lemma GreatestB_le:
fixes n :: nat
assumes xn and P x
shows x  (GREATEST k. kn  P k) 
proof -
  have *:  y. yn  P y  y<Suc n by auto
  then show x  (GREATEST k. kn  P k) using assms by (blast intro: Greatest_le_nat)
qed

lemma LeastBI_ex: assumes k  n. P k shows P (LEAST k::'c::wellorder. P k) and (LEAST k. P k)  n 
proof -
  from assms obtain k where k: "k  n" "P k" by blast
  thus P (LEAST k. P k) using LeastI[of P k] by simp
  show (LEAST k. P k)  n using Least_le[of P k] k by auto
qed

lemma allB_atLeastLessThan_lower:  assumes (i::nat)  j  x{i..<n}. P x shows  x{j..<n}. P x proof 
  fix x assume x{j..<n} hence x{i..<n} using assms(1) by simp
  thus P x using assms(2) by auto
qed


subsection ‹Facts about Paths›

context IFC
begin

lemma path0: path σ 0 = entry unfolding path_def by auto

lemma path_in_nodes[intro]: path σ k  nodes proof (induction k)
  case (Suc k)
  hence  σ'. (path σ k, suc (path σ k) σ')  edges by auto
  hence (path σ k, path σ (Suc k))  edges unfolding path_def 
    by (metis suc_def comp_apply funpow.simps(2) prod.collapse) 
  thus ?case using edges_nodes by force
qed (auto simp add: path_def)

lemma path_is_path[simp]: is_path (path σ) unfolding is_path_def path_def using step_suc_sem apply auto
by (metis path_def suc_def edges_complete path_in_nodes prod.collapse)

lemma term_path_stable: assumes is_path π π i = return and le: i  j shows π j = return 
using le proof (induction j)
  case (Suc j) 
  show ?case proof cases
    assume ij
    hence π j = return using Suc by simp
    hence (return, π (Suc j))  edges using assms(1) unfolding is_path_def by metis
    thus π (Suc j) = return using edges_return by auto
  next
    assume ¬ i  j
    hence Suc j = i using Suc by auto
    thus ?thesis using assms(2) by auto
  qed
next
  case 0 thus ?case using assms by simp
qed 

lemma path_path_shift: assumes is_path π shows is_path (π«m) 
using assms unfolding is_path_def by simp

lemma path_cons: assumes is_path π is_path π' π m = π' 0 shows is_path (π @⇗mπ') 
unfolding is_path_def proof(rule,cases)
  fix n assume m < n thus ((π @⇗mπ') n, (π @⇗mπ') (Suc n))  edges 
    using assms(2) unfolding is_path_def path_append_def
    by (auto,metis Suc_diff_Suc diff_Suc_Suc less_SucI) 
next
  fix n assume *: ¬ m < n  thus ((π @⇗mπ') n, (π @⇗mπ') (Suc n))  edges proof cases
    assume [simp]: n = m
    thus ?thesis using assms unfolding is_path_def path_append_def by force
  next
    assume n  m
    hence Suc n  m n m using * by auto
    with assms(1) show ?thesis unfolding is_path_def by auto
  qed
qed

lemma is_path_loop: assumes is_path π 0 < i π i = π 0 shows is_path (λ n. π (n mod i)) unfolding is_path_def proof (rule,cases)
  fix n
  assume 0 < Suc n mod i
  hence Suc n mod i = Suc (n mod i) by (metis mod_Suc neq0_conv)
  moreover 
  have (π (n mod i), π (Suc (n mod i)))  edges using assms(1) unfolding is_path_def by auto
  ultimately
  show (π (n mod i), π (Suc n mod i))  edges by simp
  next
  fix n
  assume ¬ 0 < Suc n mod i
  hence Suc n mod i = 0 by auto
  moreover 
  hence n mod i = i - 1 using assms(2) by (metis Zero_neq_Suc diff_Suc_1 mod_Suc)
  ultimately
  show (π(n mod i), π (Suc n mod i))  edges using assms(1) unfolding is_path_def by (metis assms(3) mod_Suc)
qed

lemma path_nodes: is_path π  π k  nodes unfolding is_path_def using edges_nodes by force 

lemma direct_path_return': assumes is_path π π 0 = x x  return π n = return
obtains π' n' where is_path π' π' 0 = x π' n' = return  i> 0. π' i  x
using assms proof (induction n arbitrary: π  rule: less_induct)
  case (less n π) 
  hence ih:  n' π'. n' < n  is_path π'  π' 0 = x  π' n' = return  thesis using assms by auto
  show thesis proof cases
    assume  i>0. π i  x thus thesis using less by auto
  next
    assume ¬ ( i>0. π i  x)
    then obtain i where 0<i π i = x by auto
    hence (π«i) 0 = x by auto
    moreover
    have i < n using less(3,5,6) π i = x by (metis linorder_neqE_nat term_path_stable less_imp_le)    
    hence (π«i) (n-i) = return using less(6) by auto
    moreover
    have is_path (π«i) using less(3) by (metis path_path_shift)
    moreover
    have n - i < n using 0<i i < n by auto    
    ultimately show thesis using ih by auto
  qed
qed

lemma direct_path_return: assumes  x  nodes x  return
obtains π n where is_path π π 0 = x π n = return  i> 0. π i  x
using direct_path_return'[of _ x] reaching_ret[OF assms(1)] assms(2) by blast

lemma path_append_eq_up_to: (π @⇗kπ') =⇘kπ  unfolding eq_up_to_def by auto

lemma eq_up_to_le: assumes k  n π =⇘nπ' shows π =⇘kπ' using assms unfolding eq_up_to_def by auto 

lemma eq_up_to_refl: shows π =⇘kπ unfolding eq_up_to_def by auto 

lemma eq_up_to_sym: assumes π =⇘kπ' shows π' =⇘kπ using assms unfolding eq_up_to_def by auto

lemma eq_up_to_apply: assumes π =⇘kπ' j  k shows π j = π' j using assms unfolding eq_up_to_def by auto

lemma path_swap_ret: assumes is_path π obtains π' n where is_path π' π =⇘kπ' π' n = return
proof -
  have nd: π k  nodes using assms path_nodes by simp
  obtain π' n where *: is_path π' π' 0 = π k π' n = return using reaching_ret[OF nd] by blast
  have π =⇘k(π@⇗kπ') by (metis eq_up_to_sym path_append_eq_up_to)
  moreover
  have is_path (π@⇗kπ') using assms * path_cons by metis
  moreover
  have (π@⇗kπ') (k + n) = return using * by auto
  ultimately
  show thesis using that by blast
qed

lemma path_suc: path σ (Suc k) = fst (step (path σ k, σk)) by (induction k, auto simp: path_def kth_state_def)

lemma kth_state_suc: σSuc k= snd (step (path σ k, σk)) by (induction k, auto simp: path_def kth_state_def)


subsection ‹Facts about Post Dominators›

lemma pd_trans: assumes 1: y pd→ x and 2: z pd→y shows z pd→x 
proof -
  {
    fix π n
    assume 3[simp]: is_path π π 0 = x π n = return
    then obtain k where π k = y and 7: k  n using 1 unfolding is_pd_def by blast
    then have (π«k) 0 = y and (π«k) (n-k) = return by auto
    moreover have is_path (π«k) by(metis 3(1) path_path_shift)
    ultimately obtain k' where 8: (π«k) k' = z and k'  n-k using 2 unfolding is_pd_def by blast
    hence k+k'n and π (k+ k') = z using 7 by auto
    hence kn. π k = z using path_nodes by auto    
  }
  thus ?thesis using 1 unfolding is_pd_def by blast
qed

lemma pd_path: assumes y pd→ x
obtains π n k where is_path π and π 0 = x and π n = return and π k = y and k  n   
using assms unfolding is_pd_def using reaching_ret[of x] by blast

lemma pd_antisym: assumes xpdy: x pd→ y and ypdx: y pd→ x shows x = y
proof -
  obtain π n where path: is_path π and π0: π 0 = x and πn: π n = return using pd_path[OF ypdx] by metis
  hence kex: kn. π k = y using ypdx unfolding is_pd_def by auto
  obtain k where k: k = (GREATEST k. kn  π k = y) by simp
  have πk: π k = y and kn: k  n using k kex by (auto intro: GreatestIB)
  
  have kpath: is_path (π«k) by (metis path_path_shift path)
  moreover have k0: (π«k) 0 = y using πk by simp
  moreover have kreturn: (π«k) (n-k) = return using kn πn by simp
  ultimately have ky': k'(n-k).(π«k) k' = x using xpdy unfolding is_pd_def by simp      

  obtain k' where k': k' = (GREATEST k'. k'(n-k)  (π«k) k' = x) by simp

  with ky' have πk': (π«k) k' = x and kn': k'  (n-k)  by (auto intro: GreatestIB)
  have k'path: is_path (π«k«k') using kpath by(metis path_path_shift)
  moreover have k'0: (π«k«k') 0 = x using πk' by simp
  moreover have k'return: (π«k«k') (n-k-k') = return using kn' kreturn by (metis path_shift_def le_add_diff_inverse)
  ultimately have ky'': k''(n-k-k').(π«k«k') k'' = y using ypdx unfolding is_pd_def by blast

  obtain k'' where k'': k''= (GREATEST k''. k''(n-k-k')  (π«k«k') k'' = y) by simp
  with ky'' have πk'': (π«k«k') k'' = y and kn'': k''  (n-k-k')  by (auto intro: GreatestIB)

  from this(1) have  π (k + k' + k'') = y by (metis path_shift_def add.commute add.left_commute)
  moreover
  have k + k' +k''  n using kn'' kn' kn by simp
  ultimately have k + k' + k'' k using k by(auto simp: GreatestB_le)
  hence k' = 0 by simp
  with k0 πk' show x = y by simp
qed

lemma pd_refl[simp]: x  nodes  x pd→ x unfolding is_pd_def by blast

lemma pdt_trans_in_pdt: (x,y)  pdt+  (x,y)  pdt 
proof (induction rule: trancl_induct)
  case base thus ?case by simp
next
  case (step y z) show ?case unfolding pdt_def proof (simp)
    have *: y pd→ x z pd→ y using step unfolding pdt_def by auto
    hence [simp]: z pd→ x using pd_trans[where x=x and y=y and z=z] by simp
    have xz proof 
      assume x = z
      hence z pd→ y y pd→ z using * by auto
      hence z = y using pd_antisym by auto
      thus False using step(2) unfolding pdt_def by simp
    qed
    thus x  z  z pd→ x by auto
  qed
qed

lemma pdt_trancl_pdt: pdt+ = pdt using pdt_trans_in_pdt by fast

lemma trans_pdt: trans pdt by (metis pdt_trancl_pdt trans_trancl)

definition [simp]: pdt_inv = pdt¯

lemma wf_pdt_inv: wf (pdt_inv) proof (rule ccontr)
  assume ¬ wf (pdt_inv)
  then obtain f where  i. (f (Suc i), f i)  pdt¯ using wf_iff_no_infinite_down_chain by force
  hence *:  i. (f i, f (Suc i))  pdt by simp
  have **: i.  j>i. (f i, f j)  pdt proof(rule,rule,rule)
    fix i j assume  i < (j::nat) thus (f i, f j)  pdt proof (induction j rule: less_induct)
      case (less k)
      show ?case proof (cases Suc i < k)
        case True
        hence k:k-1 < k i < k-1 and sk: Suc (k-1) = k by auto
        show ?thesis using less(1)[OF k] *[rule_format,of k-1,unfolded sk] trans_pdt[unfolded trans_def] by blast
      next
        case False
        hence Suc i = k using less(2) by auto
        then show ?thesis using * by auto
      qed
    qed
  qed
  hence ***: i.  j > i. f j pd→ f i  i.  j > i. f i   f j unfolding pdt_def by auto
  hence ****: i>0. f i pd→ f 0 by simp
  hence f 0  nodes  using * is_pd_def by fastforce
  then obtain π n where π:is_path π π 0 = f 0 π n = return using reaching_ret by blast  
  hence  i>0.  kn. π k = f i using ***(1) f 0  nodes unfolding is_pd_def by blast
  hence πf: i.  kn. π k = f i using π(2) by (metis le0 not_gr_zero)
  have range f  π ` {..n} proof(rule subsetI)
    fix x assume x  range f
    then obtain i where x = f i by auto
    then obtain k where x = π k k  n using πf by metis
    thus x  π ` {..n} by simp
  qed
  hence f:finite (range f) using finite_surj by auto
  hence fi: i. infinite {j. f j = f i}  using pigeonhole_infinite[OF _ f] by auto
  obtain i where infinite {j. f j = f i} using fi ..    
  thus False 
    by (metis (mono_tags, lifting) "***"(2) bounded_nat_set_is_finite gt_ex mem_Collect_eq nat_neq_iff)
qed

lemma return_pd: assumes x  nodes shows return pd→ x unfolding is_pd_def using assms by blast

lemma pd_total: assumes xz: x pd→ z and yz: y pd→ z shows x pd→ y  y pd→x 
proof -
  obtain π n where path: is_path π and π0: π 0 = z and πn: π n = return using xz reaching_ret unfolding is_pd_def by force
  have *:  kn. (π k = x  π k = y) (is  kn. ?P k) using path π0 πn xz yz unfolding is_pd_def by auto
  obtain k where k: k = (LEAST k. π k = x  π k = y) by simp
  hence kn: kn and πk: π k = x  π k = y using LeastBI_ex[OF *] by auto 
  note k_le = Least_le[where P = ?P] 
  show ?thesis proof (cases)
    assume kx: π k = x
    have k_min:  k'. π k' = y  k  k' using k_le unfolding k by auto
    {
      fix π' 
      and n' :: nat
      assume path': is_path π' and π'0: π' 0 = x and π'n': π' n' = return
      have path'': is_path (π @⇗kπ') using path_cons[OF path path'] kx π'0 by auto
      have π''0: (π @⇗kπ') 0 = z using π0 by simp
      have π''n: (π @⇗kπ') (k+n') = return using π'n' kx π'0 by auto
      obtain k' where k': k'  k + n' (π @⇗kπ') k' = y using yz path'' π''0 π''n unfolding is_pd_def by blast
      have **: k  k' proof (rule ccontr)
        assume ¬ k  k'
        hence k' < k by simp
        moreover 
        hence π k' = y using k' by auto
        ultimately
        show False using k_min by force
     qed
     hence π' (k' - k) = y using k' π'0 kx  by auto
     moreover
     have (k' - k)  n' using k' by auto
     ultimately 
     have  k n'. π' k = y by auto
   }
   hence y pd→ x using kx path_nodes path unfolding is_pd_def by auto
   thus ?thesis ..
 next ― ‹This is analogous argument›
   assume kx: π k  x
   hence ky: π k = y using πk by auto
   have k_min:  k'. π k' = x  k  k' using k_le unfolding k by auto
    {
      fix π' 
      and n' :: nat
      assume path': is_path π' and π'0: π' 0 = y and π'n': π' n' = return
      have path'': is_path (π @⇗kπ') using path_cons[OF path path'] ky π'0 by auto
      have π''0: (π @⇗kπ') 0 = z using π0 by simp
      have π''n: (π @⇗kπ') (k+n') = return using π'n' ky π'0 by auto
      obtain k' where k': k'  k + n' (π @⇗kπ') k' = x using xz path'' π''0 π''n unfolding is_pd_def by blast
      have **: k  k' proof (rule ccontr)
        assume ¬ k  k'
        hence k' < k by simp
        moreover 
        hence π k' = x using k' by auto
        ultimately
        show False using k_min by force
     qed
     hence π' (k' - k) = x using k' π'0 ky  by auto
     moreover
     have (k' - k)  n' using k' by auto
     ultimately 
     have  k n'. π' k = x by auto
   }
   hence x pd→ y using ky path_nodes path unfolding is_pd_def by auto
   thus ?thesis ..
  qed
qed    

lemma pds_finite: finite {y . (x,y)  pdt} proof cases 
  assume x  nodes
  then obtain π n where π:is_path π π 0 = x π n = return using reaching_ret by blast
  have *:  y  {y. (x,y) pdt}. y pd→ x using pdt_def by auto
  have  y  {y. (x,y) pdt}.  k  n. π k = y  using * π is_pd_def by blast
  hence {y. (x,y) pdt}  π ` {..n}  by auto
  then show ?thesis using finite_surj by blast
next
  assume ¬ x nodes
  hence {y. (x,y)pdt} = {} unfolding pdt_def is_pd_def using path_nodes reaching_ret by fastforce
  then show ?thesis by simp
qed

lemma ipd_exists: assumes node: x  nodes and not_ret: xreturn shows y. y ipd→ x 
proof -
  let ?Q = {y. xy  y pd→ x}
  have *: return  ?Q using assms return_pd by simp    
  hence **:  x. x ?Q by auto
  have fin: finite ?Q using pds_finite unfolding pdt_def by auto
  have tot:  y z. y?Q  z  ?Q  z pd→ y  y pd→ z using pd_total by auto
  obtain y where ymax: y ?Q  z?Q. z = y  z pd→ y using fin ** tot proof (induct)
    case empty
    then show ?case by auto
  next
    case (insert x F) show thesis proof (cases F = {})
      assume F = {}
      thus thesis using insert(4)[of x] by auto
    next  
      assume F  {}
      hence  x. x F by auto
      have y. y  F  zF. z = y  z pd→ y  thesis proof -
        fix y assume a: y  F zF. z = y  z pd→ y
        have x  y using insert a by auto
        have x pd→ y  y pd→ x using insert(6) a(1) by auto
        thus thesis proof 
          assume x pd→ y
          hence zinsert x F. z = y  z pd→ y using a(2) by blast
          thus thesis using a(1) insert(4) by blast
        next
          assume y pd→ x
          have zinsert x F. z = x  z pd→ x proof
            fix z assume z insert x F thus z = x  z pd→ x proof(rule,simp)
              assume zF
              hence z = y  z pd→ y using a(2) by auto
              thus z = x  z pd→ x proof(rule,simp add: y pd→ x)
                assume z pd→ y
                show z = x  z pd→ x using y pd→ x z pd→ y pd_trans by blast
              qed 
            qed
          qed 
          then show thesis using insert by blast
        qed
      qed
      then show thesis using insert by blast
    qed
  qed    
  hence ***: y pd→ x xy by auto
  have  z. z  x  z pd→ x  z pd→ y proof (rule,rule)
    fix z 
    assume a: z  x  z pd→ x
    hence b: z  ?Q by auto
    have y pd→ z  z pd→ y using pd_total ***(1) a by auto
    thus z pd→ y proof
      assume c: y pd→ z
      hence y = z using b ymax pdt_def pd_antisym by auto
      thus z pd→ y using c by simp
    qed simp
  qed
  with *** have  y ipd→ x unfolding is_ipd_def by simp
  thus ?thesis by blast
qed

lemma ipd_unique: assumes yipd: y ipd→ x and y'ipd: y' ipd→ x shows y = y' 
proof -  
  have 1: y pd→ y' and  2: y' pd→ y using yipd y'ipd unfolding is_ipd_def by auto
  show ?thesis using pd_antisym[OF 1 2] .
qed

lemma ipd_is_ipd: assumes x  nodes and xreturn shows ipd x ipd→ x proof -
  from assms obtain y where y ipd→ x using ipd_exists by auto
  moreover
  hence  z. z ipd→x  z = y using ipd_unique by simp
  ultimately show ?thesis unfolding ipd_def by (auto intro: theI2)
qed

lemma is_ipd_in_pdt: y ipd→ x  (x,y)  pdt unfolding is_ipd_def pdt_def by auto

lemma ipd_in_pdt: x  nodes  xreturn  (x,ipd x)  pdt by (metis ipd_is_ipd is_ipd_in_pdt)

lemma no_pd_path: assumes x  nodes and ¬ y pd→ x
obtains π n where is_path π and π 0 = x and π n = return and  k  n. π k  y
proof (rule ccontr)
  assume ¬ thesis
  hence  π n.  is_path π  π 0 = x  π n = return  ( kn . π k = y) using that by force
  thus False using assms unfolding is_pd_def by auto
qed

lemma pd_pd_ipd: assumes x  nodes xreturn yx y pd→ x shows y pd→ ipd x 
proof -
  have ipd x pd→ x by (metis assms(1,2) ipd_is_ipd is_ipd_def)
  hence y pd→ ipd x  ipd x pd→ y by (metis assms(4) pd_total)
  thus ?thesis proof
    have 1: ipd x ipd→ x by (metis assms(1,2) ipd_is_ipd)
    moreover
    assume ipd x pd→ y
    ultimately
    show y pd→ ipd x unfolding is_ipd_def using assms(3,4) by auto
  qed auto
qed

lemma pd_nodes: assumes y pd→ x shows pd_node1: y  nodes and pd_node2: x  nodes
proof -
  obtain π k where is_path π π k = y using assms unfolding is_pd_def using reaching_ret by force
  thus y  nodes using path_nodes by auto
  show x  nodes using assms unfolding is_pd_def by simp
qed

lemma pd_ret_is_ret: x pd→ return  x = return by (metis pd_antisym pd_node1 return_pd)

lemma ret_path_none_pd: assumes x  nodes xreturn 
obtains π n where is_path π  π 0 = x π n = return   i>0. ¬ x pd→ π i
proof(rule ccontr)
  assume ¬thesis
  hence *:  π n. is_path π; π 0 = x; π n = return  i>0. x pd→ π i using that by blast
  obtain π n where **: is_path π  π 0 = x π n = return  i>0. π i  x using direct_path_return[OF assms] by metis
  then obtain i where ***: i>0 x pd→ π i using * by blast
  hence π i  return using pd_ret_is_ret assms(2) by auto
  hence i < n using assms(2) term_path_stable ** by (metis linorder_neqE_nat less_imp_le)
  hence (π«i)(n-i) = return using **(3) by auto
  moreover
  have (π«i) (0) = π i by simp
  moreover 
  have is_path (π«i) using **(1) path_path_shift by metis
  ultimately
  obtain k where (π«i) k = x using ***(2) unfolding is_pd_def by metis
  hence π (i + k) = x by auto
  thus False using **(4) i>0 by auto
qed

lemma path_pd_ipd0': assumes is_path π and π n  return π n  π 0 and π n pd→ π 0 
obtains k where k  n and π k = ipd(π 0) 
proof(rule ccontr)  
  have *: π n pd→ ipd (π 0) by (metis is_pd_def assms(3,4) pd_pd_ipd pd_ret_is_ret)  
  obtain π' n' where **: is_path π' π' 0 = π n π' n' = return  i>0. ¬ π n pd→ π' i  by (metis assms(2) assms(4) pd_node1 ret_path_none_pd)
  hence  i>0. π' i  ipd (π 0) using * by metis
  moreover
  assume ¬ thesis
  hence  kn. π k  ipd (π 0) using that by blast
  ultimately
  have  i. (π@⇗nπ') i  ipd (π 0) by (metis diff_is_0_eq neq0_conv path_append_def)
  moreover
  have (π@⇗nπ') (n + n') = return 
    by (metis π' 0 = π n π' n' = return add_diff_cancel_left' assms(2) diff_is_0_eq path_append_def)
  moreover
  have (π@⇗nπ') 0 = π 0 by (metis le0 path_append_def)
  moreover
  have is_path (π@⇗nπ') by (metis π' 0 = π n is_path π' assms(1) path_cons)
  moreover  
  have ipd (π 0) pd→ π 0 by (metis **(2,3,4) assms(2) assms(4) ipd_is_ipd is_ipd_def neq0_conv pd_node2)
  moreover
  have π 0  nodes by (metis assms(1) path_nodes)
  ultimately
  show False unfolding is_pd_def by blast
qed

lemma path_pd_ipd0: assumes is_path π and π 0  return π n  π 0 and π n pd→ π 0 
obtains k where k  n and π k = ipd(π 0) 
proof cases 
  assume *: π n = return
  have ipd (π 0) pd→ (π 0) by (metis is_ipd_def is_pd_def assms(2,4) ipd_is_ipd)
  with assms(1,2,3) * show thesis unfolding is_pd_def by (metis that)
next
  assume π n  return 
  from path_pd_ipd0' [OF assms(1) this assms(3,4)] that show thesis by auto
qed

lemma path_pd_ipd: assumes is_path π and π k  return π n  π k and π n pd→ π k and kn: k < n 
obtains l where k < l and l  n and π l = ipd(π k) 
proof -
  have is_path (π « k) (π « k) 0  return (π « k) (n - k)  (π « k) 0 (π « k) (n - k) pd→ (π « k) 0 
  using assms path_path_shift by auto 
  with path_pd_ipd0[of π«k n-k]
  obtain ka where ka  n - k (π « k) ka = ipd ((π « k) 0) .
  hence k + ka  n π (k + ka) = ipd (π k) using kn by auto
  moreover 
  hence π (k + ka) ipd→ π k by (metis assms(1) assms(2) ipd_is_ipd path_nodes)
  hence k < k + ka unfolding is_ipd_def by (metis nat_neq_iff not_add_less1)
  ultimately
  show thesis using that[of k+ka] by auto
qed

lemma path_ret_ipd: assumes is_path π and π k  return π n = return 
obtains l where k < l and l  n and π l = ipd(π k) 
proof -
  have π n  π k using assms by auto
  moreover
  have k  n apply (rule ccontr) using term_path_stable assms by auto
  hence k < n by (metis assms(2,3) dual_order.order_iff_strict)
  moreover
  have π n pd→ π k by (metis assms(1,3) path_nodes return_pd)
  ultimately
  obtain l where k < l l  n π l = ipd (π k) using assms path_pd_ipd by blast
  thus thesis using that by auto
qed

lemma pd_intro: assumes l pd→ k is_path π π 0 = k π n = return 
obtains i where i  n π i = l using assms unfolding is_pd_def by metis

lemma path_pd_pd0: assumes path:  is_path π and lpdn: π l pd→ n and npd0: n pd→ π 0 
obtains k where k  l π k = n
proof (rule ccontr)
  assume ¬ thesis
  hence notn:  k. k  l  π k  n using that by blast
  have nret: π l  return by (metis is_pd_def assms(1,3) notn)
  
  obtain π' n' where path': is_path π' and π0': π' 0 = π l and πn': π' n' = return and nonepd:  i>0. ¬ π l pd→ π' i
  using nret path path_nodes ret_path_none_pd by metis
  
  have π l  n using notn by simp
  hence  i. π' i  n using nonepd π0' lpdn by (metis neq0_conv)
  
  hence notn':  i. (π@⇗lπ') i  n using notn π0' by auto

  have is_path (π@⇗lπ') using path path' by (metis π0' path_cons)
  moreover
  have (π@⇗lπ') 0 = π 0 by simp
  moreover
  have (π@⇗lπ') (n' + l) = return using π0' πn' by auto
  ultimately
  show False using notn' npd0 unfolding is_pd_def by blast
qed


subsection ‹Facts about Control Dependencies›

lemma icd_imp_cd: n icd⇗π⇖→ k  n cd⇗π⇖→ k by (metis is_icdi_def)

lemma ipd_impl_not_cd:  assumes j  {k..i} and π j = ipd (π k) shows ¬ i cd⇗π⇖→ k 
  by (metis assms(1) assms(2) is_cdi_def)

lemma cd_not_ret: assumes i cd⇗π⇖→ k shows π k  return by (metis is_cdi_def assms nat_less_le term_path_stable)

lemma cd_path_shift: assumes j  k is_path π shows (i cd⇗π⇖→ k) = (i - j cd⇗π«j⇖→ k-j) proof 
  assume a: i cd⇗π⇖→ k
  hence b: k < i by (metis is_cdi_def)
  hence is_path (π « j) k - j < i - j using assms apply (metis path_path_shift) 
  by (metis assms(1) b diff_less_mono)  
  moreover 
  have c:  j  {k..i}. π j  ipd (π k) by (metis a ipd_impl_not_cd)
  hence  ja  {k - j..i - j}. (π « j) ja  ipd ((π « j) (k - j)) using b assms by auto fastforce
  moreover 
  have j < i using assms(1) b by auto
  hence (π«j) (i - j)  return using a unfolding is_cdi_def by auto 
  ultimately
  show i - j cd⇗π«j⇖→ k-j unfolding is_cdi_def by simp
next
  assume a: i - j cd⇗π«j⇖→ k-j
  hence b: k - j < i-j by (metis is_cdi_def)
  moreover
  have c:  ja  {k - j..i - j}. (π « j) ja  ipd ((π « j) (k - j)) by (metis a ipd_impl_not_cd)
  have  j  {k..i}. π j  ipd (π k) proof (rule,goal_cases) case (1 n)
    hence n-j  {k-j..i-j} using assms by auto
    hence π (j + (n-j))  ipd(π (j + (k-j))) by (metis c path_shift_def)
    thus ?case using 1 assms(1) by auto
  qed
  moreover
  have j < i using assms(1) b by auto
  hence π i  return using a unfolding is_cdi_def by auto
  ultimately
  show i cd⇗π⇖→k unfolding is_cdi_def by (metis assms(1) assms(2) diff_is_0_eq' le_diff_iff nat_le_linear nat_less_le)
qed 

lemma cd_path_shift0: assumes is_path π shows (i cd⇗π⇖→ k) = (i-k cd⇗π«k⇖→0)
  using cd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)

lemma icd_path_shift: assumes l  k is_path π shows (i icd⇗π⇖→ k) = (i - l icd⇗π«l⇖→ k - l) 
proof -
  have is_path (π«l) using path_path_shift assms(2) by auto
  moreover
  have (i cd⇗π⇖→ k) = (i - l cd⇗π«l⇖→ k - l) using assms cd_path_shift by auto
  moreover 
  have ( m  {k<..<i}. ¬ i cd⇗π⇖→ m) = ( m  {k - l<..<i - l}. ¬ i - l cd⇗π « l⇖→ m) 
  proof -
    {fix m assume *:  m  {k - l<..<i - l}. ¬ i - l cd⇗π « l⇖→ m m  {k<..<i} 
      hence m-l  {k-l<..<i-l} using assms(1) by auto
      hence ¬ i - l cd⇗π«l⇖→(m-l) using * by blast
      moreover
      have l  m using * assms by auto
      ultimately have ¬ i cd⇗π⇖→m using assms(2) cd_path_shift by blast
    }
    moreover
    {fix m assume *:  m  {k<..<i}. ¬ i cd⇗π⇖→ m m-l  {k-l<..<i-l} 
      hence m  {k<..<i} using assms(1) by auto
      hence ¬ i cd⇗π⇖→m using * by blast
      moreover
      have l  m using * assms by auto
      ultimately have ¬ i - l cd⇗π«l⇖→(m-l) using assms(2) cd_path_shift by blast
    }
    ultimately show ?thesis by auto (metis diff_add_inverse)
  qed
  ultimately
  show ?thesis unfolding is_icdi_def using assms by blast
qed

lemma icd_path_shift0: assumes is_path π shows (i icd⇗π⇖→ k) = (i-k icd⇗π«k⇖→0)
  using icd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)

lemma cdi_path_swap: assumes is_path π' j cd⇗π⇖→k π =⇘jπ' shows j cd⇗π'⇖→k using assms unfolding eq_up_to_def is_cdi_def by auto

lemma cdi_path_swap_le: assumes is_path π' j cd⇗π⇖→k π =⇘nπ' j  n shows j cd⇗π'⇖→k by (metis assms cdi_path_swap eq_up_to_le)

lemma not_cd_impl_ipd:  assumes is_path π and k < i and ¬ i cd⇗π⇖→ k and π i  return obtains j where j  {k..i} and π j = ipd (π k)
by (metis assms(1) assms(2) assms(3) assms(4) is_cdi_def)

lemma icd_is_the_icd: assumes i icd⇗π⇖→ k shows k = (THE k. i icd⇗π⇖→ k) using assms icd_uniq 
  by (metis the1_equality)

lemma all_ipd_imp_ret: assumes is_path π and  i. π i  return  ( j>i. π j = ipd (π i)) shows j. π j = return
proof - 
  { fix x assume *: π 0 = x
    have ?thesis using wf_pdt_inv * assms  
    proof(induction x arbitrary: π rule: wf_induct_rule )
    case (less x π) show ?case proof (cases x = return)
      case True thus ?thesis using less(2) by auto
    next
      assume not_ret: x  return
      moreover
      then obtain k where k_ipd: π k = ipd x using less(2,4) by auto
      moreover  
      have x  nodes using less(2,3) by (metis path_nodes)
      ultimately 
      have (x, π k)  pdt by (metis ipd_in_pdt)
      hence a: (π k, x)  pdt_inv unfolding pdt_inv_def by simp     
      have b: is_path (π « k) by (metis less.prems(2) path_path_shift)    
      have c:  i. (π«k) i  return  (j>i. (π«k) j = ipd ((π«k) i)) using less(4) apply auto
        by (metis (full_types) ab_semigroup_add_class.add_ac(1) less_add_same_cancel1 less_imp_add_positive)
      from less(1)[OF a _ b c]
      have j. (π«k) j = return by auto    
      thus j. π j = return by auto
    qed
    qed
  }
  thus ?thesis by simp
qed

lemma loop_has_cd: assumes is_path π 0 < i π i = π 0 π 0  return shows  k < i. i cd⇗π⇖→ k proof (rule ccontr)
  let  = (λ n. π (n mod i))  
  assume ¬ (k<i. i cd⇗π⇖→ k)
  hence  k <i. ¬ i cd⇗π⇖→ k by blast
  hence *:  k<i. (j  {k..i}. π j = ipd (π k)) using assms(1,3,4) not_cd_impl_ipd by metis
  have  k. ( j > k.  j = ipd ( k)) proof 
    fix k
    have k mod i < i using assms(2) by auto
    with * obtain j where j  {(k mod i)..i} π j = ipd (π (k mod i)) by auto
    then obtain j' where 1: j' < i π j' = ipd (π (k mod i)) 
      by (cases j = i, auto ,metis assms(2) assms(3),metis le_neq_implies_less)
    then obtain j'' where 2: j'' > k j'' mod i = j' by (metis mod_bound_instance)
    hence  j'' = ipd ( k) using 1 by auto
    with 2(1)
    show  j > k.  j = ipd ( k) by auto
  qed
  moreover 
  have is_path  by (metis assms(1) assms(2) assms(3) is_path_loop)
  ultimately 
  obtain k where  k = return by (metis (lifting) all_ipd_imp_ret)
  moreover 
  have k mod i < i by (simp add: assms(2)) 
  ultimately
  have π i = return by (metis assms(1) term_path_stable less_imp_le)
  thus False by (metis assms(3) assms(4))
qed

lemma loop_has_cd': assumes is_path π j < i π i = π j π j  return shows  k  {j..<i}. i cd⇗π⇖→ k 
proof -
  have  k'< i-j. i-j cd⇗π«j⇖→k' 
    apply(rule loop_has_cd) 
    apply (metis assms(1) path_path_shift)
    apply (auto simp add: assms less_imp_le)
    done
  then obtain k where k: k<i-j i-j cd⇗π«j⇖→k by auto
  hence k': (k+j) < i  i-j cd⇗π«j⇖→ (k+j)-j  by auto
  note cd_path_shift[OF _ assms(1)]
  hence i cd⇗π⇖→ k+j using k'(2) by (metis le_add1 add.commute)
  with k'(1) show ?thesis by force
qed  

lemma claim'': assumes pathπ: is_path π and pathπ': is_path π' 
and πi: π i = π' i' and πj: π j = π' j' 
and not_cd:   k. ¬ j cd⇗π⇖→ k   k. ¬ i' cd⇗π'⇖→ k 
and nret: π i  return
and ilj: i < j
shows i' < j' proof (rule ccontr)
  assume ¬ i' < j'  
  hence jlei: j'  i' by auto
  show False proof (cases)
  assume j'li': j' < i' 
  define π'' where π''  (π@⇗j(π'«j'))«i
  note π''_def[simp]
  have π j = (π' « j') 0 by (metis path_shift_def Nat.add_0_right πj)
  hence is_path π'' using pathπ pathπ' π''_def path_path_shift path_cons by presburger
  moreover 
  have π'' (j-i+(i'-j')) = π'' 0  using ilj jlei πi πj 
    by (auto, metis add_diff_cancel_left' le_antisym le_diff_conv le_eq_less_or_eq)
  moreover
  have π'' 0  return by (simp add: ilj less_or_eq_imp_le nret)
  moreover
  have 0 < j-i+(i'-j') by (metis add_is_0 ilj neq0_conv zero_less_diff)
  ultimately obtain k where k: k < j-i+(i'-j') j-i+(i'-j') cd⇗π''⇖→ k   by (metis loop_has_cd)
  hence *:  l  {k..j-i+(i'-j')}. π'' l  ipd (π'' k) by (metis is_cdi_def)
  show False proof (cases k < j-i)
    assume a: k < j - i
    hence b: π'' k = π (i + k) by auto
    have  l  {i+k..j}. π l  ipd (π (i+k)) proof
      fix l assume l: l  {i + k..j}
      hence π l = π'' (l - i) by auto
      moreover 
      from a l have l-i  {k .. j-i + (i'-j')} by force
      ultimately show π l  ipd (π (i + k)) using * b by auto
    qed
    moreover 
    have i + k < j using a by simp
    moreover
    have π j  return by (metis πi πj j'li' nret pathπ' term_path_stable less_imp_le) 
    ultimately
    have j cd⇗π⇖→ i+k  by (metis not_cd_impl_ipd pathπ)
    thus False by (metis not_cd(1))
  next
    assume ¬ k < j - i
    hence a: j - i  k by simp
    hence b: π'' k = π' (j' + (i + k) - j) unfolding π''_def path_shift_def path_append_def using ilj 
      by(auto,metis πj add_diff_cancel_left' le_antisym le_diff_conv add.commute)
    have  l  {j' + (i+k) - j..i'}. π' l  ipd (π' (j' + (i+k) - j)) proof
      fix l assume l: l  {j' + (i+k) - j..i'}
      hence π' l = π'' (j + l - i - j') unfolding π''_def path_shift_def path_append_def using ilj
        by (auto, metis Nat.diff_add_assoc πj a add.commute add_diff_cancel_left' add_leD1 le_antisym le_diff_conv)
      moreover 
      from a l have j + l - i - j'  {k .. j-i + (i'-j')} by force
      ultimately show π' l  ipd (π' (j' + (i + k) - j)) using * b by auto
    qed
    moreover 
    have j' + (i+k) - j < i' using a  j'li' ilj k(1) by linarith      
    moreover 
    have π' i'  return by (metis πi nret)
    ultimately    
    have i' cd⇗π'⇖→ j' + (i+k) - j by (metis not_cd_impl_ipd pathπ')
    thus False by (metis not_cd(2))
  qed
  next
  assume ¬ j' < i'
  hence j' = i' by (metis ¬ i' < j' linorder_cases)
  hence π i = π j by (metis πi πj)
  thus False by (metis ilj loop_has_cd' not_cd(1) nret pathπ)
qed
qed

lemma other_claim': assumes path: is_path π and eq: π i = π j and π i  return 
and icd:  k. ¬ i cd⇗π⇖→ k and  k. ¬ j cd⇗π⇖→ k shows i = j  
proof (rule ccontr,cases)
  assume i < j thus False using assms claim'' by blast
next
  assume ¬ i < j i  j 
  hence j < i by auto
  thus False using assms claim'' by (metis loop_has_cd')
qed  

lemma icd_no_cd_path_shift: assumes i icd⇗π⇖→ 0 shows ( k. ¬ i - 1 cd⇗π«1⇖→ k) 
proof (rule,rule ccontr,goal_cases)
  case (1 k)
  hence *: i - 1 cd⇗π « 1⇖→ k by simp
  have **: 1  k + 1 by simp
  have ***: is_path π by (metis assms is_icdi_def)
  hence i cd⇗π⇖→ k+1 using cd_path_shift[OF ** ***] * by auto
  moreover 
  hence k+1 < i unfolding is_cdi_def by simp
  moreover
  have 0 < k + 1 by simp
  ultimately show False using assms[unfolded is_icdi_def] by auto
qed

lemma claim': assumes pathπ: is_path π and pathπ': is_path π' and
  πi: π i = π' i' and πj: π j = π' j' and not_cd:
  i icd⇗π⇖→ 0 j icd⇗π⇖→ 0
  i' icd⇗π'⇖→ 0 j' icd⇗π'⇖→ 0
   and ilj: i < j
   and nret: π i  return
  shows i' < j' 
proof -
  have g0: 0 < i 0 < j 0 < i' 0 < j'using not_cd[unfolded is_icdi_def is_cdi_def] by auto
  have  (π « 1) (i - 1) = (π' « 1) (i' - 1) (π « 1) (j - 1) = (π' « 1) (j' - 1) using πi πj g0 by auto
  moreover
  have  k. ¬ (j - 1) cd⇗π«1⇖→ k  k. ¬ (i' - 1) cd⇗π'«1⇖→ k 
    by (metis icd_no_cd_path_shift not_cd(2)) (metis icd_no_cd_path_shift not_cd(3))
  moreover
  have is_path (π«1) is_path (π'«1) using pathπ pathπ' path_path_shift by blast+
  moreover 
  have (π«1) (i - 1)  return using g0 nret by auto
  moreover 
  have i - 1 < j - 1 using g0 ilj by auto
  ultimately have i' - 1 < j' - 1 using claim'' by blast
  thus i'<j' by auto
qed

lemma other_claim: assumes path: is_path π and eq: π i = π j and π i  return 
and icd: i icd⇗π⇖→ 0 and j icd⇗π⇖→ 0 shows i = j  proof (rule ccontr,cases)
  assume i < j thus False using assms claim' by blast
next
  assume ¬ i < j i  j 
  hence j < i by auto
  thus False using assms claim' by (metis less_not_refl)
qed

lemma cd_trans0: assumes j cd⇗π⇖→ 0 and k cd⇗π⇖→j shows k cd⇗π⇖→ 0 proof (rule ccontr)    
  have path: is_path π and ij: 0 < j and jk: j < k 
  and nret: π j  return π k  return
  and noipdi:  l  {0..j}. π l  ipd (π 0)
  and noipdj:  l  {j..k}. π l  ipd (π j)
  using assms unfolding is_cdi_def by auto
  assume ¬ k cd⇗π⇖→ 0
  hence l  {0..k}. π l = ipd (π 0) unfolding is_cdi_def using path ij jk nret by force
  then obtain l where l  {0..k} and l: π l = ipd (π 0) by auto
  hence jl: j<l and lk: lk using noipdi ij by auto
  have pdj: ipd (π 0) pd→ π j proof (rule ccontr)    
    have π j  nodes using path by (metis path_nodes)
    moreover 
    assume ¬ ipd (π 0) pd→ π j
    ultimately
    obtain π' n where *: is_path π' π' 0 = π j π' n = return  kn. π' k  ipd(π 0) using no_pd_path by metis
    hence path': is_path (π @⇗jπ') by (metis path path_cons) 
    moreover
    have  k  j + n. (π@⇗jπ') k  ipd (π 0) using noipdi *(4) by auto
    moreover 
    have (π@⇗jπ') 0 = π 0 by auto
    moreover
    have (π@⇗jπ') (j + n) = return using *(2,3) by auto
    ultimately
    have ¬ ipd (π 0) pd→ π 0 unfolding is_pd_def by metis
    thus False by (metis is_ipd_def ij ipd_is_ipd nret(1) path path_nodes term_path_stable less_imp_le)
  qed
  hence (π«j) (l-j) pd→ (π«j) 0 using jl l by auto
  moreover
  have is_path (π«j) by (metis path path_path_shift)
  moreover
  have π l  return by (metis lk nret(2) path term_path_stable)
  hence (π«j) (l-j)  return using jl by auto
  moreover 
  have π j  ipd (π 0) using noipdi by force
  hence (π«j) (l-j)  (π«j) 0 using jl l by auto
  ultimately
  obtain k' where k'  l-j and (π«j) k' = ipd ((π«j) 0) using path_pd_ipd0' by blast
  hence j + k'  {j..k} π (j+k') = ipd (π j) using jl lk by auto
  thus False using noipdj by auto
qed

lemma cd_trans: assumes j cd⇗π⇖→ i and k cd⇗π⇖→j shows k cd⇗π⇖→ i proof -
  have path: is_path π using assms is_cdi_def by auto
  have ij: i<j using assms is_cdi_def by auto
  let  = π«i
  have j-i cd⇗⇖→ 0 using assms(1) cd_path_shift0 path by auto
  moreover
  have k-i cd⇗⇖→j-i by (metis assms(2) cd_path_shift is_cdi_def ij less_imp_le_nat)
  ultimately
  have k-i cd⇗⇖→ 0 using cd_trans0 by auto
  thus k cd⇗π⇖→ i using path cd_path_shift0 by auto
qed

lemma excd_impl_exicd: assumes  k. i cd⇗π⇖→k shows  k. i icd⇗π⇖→k 
using assms proof(induction i arbitrary: π rule: less_induct)
  case (less i) 
  then obtain k where k: i cd⇗π⇖→k by auto
  hence ip: is_path π unfolding is_cdi_def by auto
  show ?case proof (cases)
    assume *:  m  {k<..<i}. ¬ i cd⇗π⇖→ m
    hence i icd⇗π⇖→k using k ip unfolding is_icdi_def by auto
    thus ?case by auto
  next
    assume ¬ ( m  {k<..<i}. ¬ i cd⇗π⇖→ m)
    then obtain m where m: m  {k<..<i} i cd⇗π⇖→ m by blast
    hence i - m cd⇗π«m⇖→ 0 by (metis cd_path_shift0 is_cdi_def)
    moreover 
    have i - m < i using m by auto
    ultimately
    obtain k' where k': i - m icd⇗π«m⇖→ k' using less(1) by blast
    hence i icd⇗π⇖→ k' + m using ip 
    by (metis add.commute add_diff_cancel_right' icd_path_shift le_add1)
    thus ?case by auto
  qed
qed

lemma cd_split: assumes i cd⇗π⇖→ k and ¬ i icd⇗π⇖→ k obtains m where i icd⇗π⇖→ m and m cd⇗π⇖→ k 
proof -
  have ki: k < i using assms is_cdi_def by auto
  obtain m where m: i icd⇗π⇖→ m using assms(1) by (metis excd_impl_exicd)
  hence k  m unfolding is_icdi_def using ki assms(1) by force
  hence km: k < musing m assms(2) by (metis le_eq_less_or_eq)
  moreover have π m  return using m unfolding is_icdi_def is_cdi_def by (simp, metis term_path_stable less_imp_le)
  moreover have m<i using m unfolding is_cdi_def is_icdi_def by auto
  ultimately 
  have m cd⇗π⇖→ k using assms(1) unfolding is_cdi_def by auto
  with m that show thesis by auto
qed

lemma cd_induct[consumes 1, case_names base IS]: assumes prem: i cd⇗π⇖→ k and base:  i. i icd⇗π⇖→k  P i 
and IH:  k' i'. k' cd⇗π⇖→ k  P k'  i' icd⇗π⇖→ k'  P i' shows P i 
using prem IH proof (induction i rule: less_induct,cases)
  case (less i) 
  assume i icd⇗π⇖→ k
  thus P i using base by simp
next
  case (less i')
  assume ¬ i' icd⇗π⇖→ k
  then obtain k' where k': i' icd⇗π⇖→ k' k' cd⇗π⇖→ k using less cd_split by blast
  hence icdk: i' cd⇗π⇖→ k' using is_icdi_def by auto
  note ih=less(3)[OF k'(2)  _ k'(1)]
  have ki: k' < i' using k' is_icdi_def is_cdi_def by auto
  have P k' using less(1)[OF ki k'(2) ] less(3) by auto
  thus P i' using ih by simp
qed

lemma cdi_prefix: n cd⇗π⇖→ m  m < n'  n'  n  n' cd⇗π⇖→ m  unfolding is_cdi_def 
  by (simp, metis term_path_stable)

lemma cr_wn': assumes 1: n cd⇗π⇖→ m and nc: ¬ m' cd⇗π⇖→ m and 3: m < m' shows n < m'
proof (rule ccontr)
  assume ¬ n < m'
  hence m'  n by simp  
  hence m' cd⇗π⇖→ m by (metis 1 3 cdi_prefix)
  thus False using nc by simp
qed

lemma cr_wn'': assumes i cd⇗π⇖→ m and j cd⇗π⇖→ n and ¬ m cd⇗π⇖→ n and  i  j shows m  n proof (rule ccontr) 
  assume ¬mn
  hence nm: n < m by auto
  moreover 
  have m<j using assms(1) assms(4) unfolding is_cdi_def by auto
  ultimately 
  have m cd⇗π⇖→ n using assms(2) cdi_prefix by auto
  thus False using assms(3) by auto
qed

lemma ret_no_cd: assumes π n = return shows ¬ n cd⇗π⇖→ k by (metis assms is_cdi_def)

lemma ipd_not_self: assumes x  nodes x return shows x  ipd x by (metis is_ipd_def assms ipd_is_ipd)

lemma icd_cs: assumes l icd⇗π⇖→k shows ‹cs⇗πl = cs⇗πk @ [π l]
proof -
  from assms have k = (THE k. l icd⇗π⇖→ k) by (metis icd_is_the_icd)
  with assms show ?thesis by auto
qed

lemma cd_not_pd: assumes l cd⇗π⇖→ k π l  π k shows ¬ π l pd→ π k proof
  assume pd: π l pd→ π k
  have nret: π k  return by (metis assms(1) pd pd_ret_is_ret ret_no_cd)
  have kl: k < l by (metis is_cdi_def assms(1))
  have path: is_path π by (metis is_cdi_def assms(1))
  from path_pd_ipd[OF path nret assms(2) pd kl]
  obtain n where k < n n  l π n = ipd (π k) .
  thus False using assms(1) unfolding is_cdi_def by auto
qed

lemma cd_ipd_is_cd: assumes k<m π m = ipd (π k)  n  {k..<m}. π n  ipd (π k) and mcdj: m cd⇗π⇖→ j shows k cd⇗π⇖→ j proof cases
  assume j < k thus k cd⇗π⇖→ j by (metis mcdj assms(1) cdi_prefix less_imp_le_nat)
next
  assume ¬ j < k
  hence kj: k  j by simp 
  have k < j apply (rule ccontr) using kj assms mcdj by (auto, metis is_cdi_def is_ipd_def cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
  moreover 
  have j < m using mcdj is_cdi_def by auto
  hence  n  {k..j}. π n  ipd(π k) using assms(3) by force
  ultimately
  have j cd⇗π⇖→ k by (metis mcdj is_cdi_def term_path_stable less_imp_le)
  hence m cd⇗π⇖→ k by (metis mcdj cd_trans)
  hence False by (metis is_cdi_def is_ipd_def assms(2) cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
  thus ?thesis by simp
qed

lemma ipd_pd_cd0: assumes lcd: n cd⇗π⇖→ 0 shows ipd (π 0) pd→ (π n) 
proof -
  obtain k l where π0: π 0 = k and πn: π n = l and cdi: n cd⇗π⇖→ 0 using lcd unfolding is_cdi_def by blast
  have nret: k  return by (metis is_cdi_def π0 cdi term_path_stable less_imp_le)
  have  path: is_path π and ipd:  in. π i  ipd k using cdi unfolding is_cdi_def π0 by auto
  {
    fix π' n'
    assume path': is_path π'
    and π'0: π' 0 = l
    and ret: π' n' = return
    have is_path (π @⇗nπ') using path path' πn π'0 by (metis path_cons)
    moreover
    have (π @⇗nπ') (n+n') = return using ret πn π'0 by auto
    moreover
    have (π @⇗nπ') 0 = k using π0 by auto
    moreover    
    have ipd k pd→ k by (metis is_ipd_def path π0 ipd_is_ipd nret path_nodes)
    ultimately
    obtain k' where k': k'  n+n' (π @⇗nπ') k' = ipd k by (metis pd_intro)
    have ¬ k' n proof 
      assume k'  n 
      hence (π @⇗nπ') k' = π k' by auto
      thus False using k'(2) ipd by (metis k'  n)
    qed
    hence (π @⇗nπ') k' = π' (k' - n) by auto
    moreover 
    have (k' - n)  n' using k' by simp
    ultimately
    have  k'n'. π' k' = ipd k unfolding k' by auto
  }
  moreover
  have l  nodes by (metis πn path path_nodes)
  ultimately show ipd (π 0) pd→ (π n) unfolding is_pd_def  by (simp add: π0 πn) 
qed

lemma ipd_pd_cd: assumes lcd: l cd⇗π⇖→ k shows ipd (π k) pd→ (π l) 
proof - 
  have l-k cd⇗π«k⇖→0 using lcd cd_path_shift0 is_cdi_def by blast 
  moreover
  note ipd_pd_cd0[OF this]
  moreover 
  have (π « k) 0 = π k by auto
  moreover
  have k < l using lcd unfolding is_cdi_def by simp
  then have (π « k) (l - k) = π l by simp 
  ultimately show ?thesis by simp
qed

lemma cd_is_cd_ipd: assumes km: k<m and ipd: π m = ipd (π k)  n  {k..<m}. π n  ipd (π k) and cdj: k cd⇗π⇖→ j and nipdj: ipd (π j)  π m shows m cd⇗π⇖→ j proof -
  have path: is_path π 
  and jk: j < k 
  and nretj: π k  return 
  and nipd:  l  {j..k}. π l  ipd (π j) using  cdj is_cdi_def by auto
  have pd: ipd (π j) pd→ π m by (metis atLeastAtMost_iff cdj ipd(1) ipd_pd_cd jk le_refl less_imp_le nipd nretj path path_nodes pd_pd_ipd)  
  have nretm: π m  return by (metis nipdj pd pd_ret_is_ret)
  have jm: j < m using jk km by simp
  show m cd⇗π⇖→ j proof (rule ccontr)
    assume ncdj: ¬ m cd⇗π⇖→ j     
    hence  l  {j..m}. π l = ipd (π j) unfolding is_cdi_def by (metis jm nretm path)
    then obtain l 
    where jl: j  l and l  m 
    and lipd: π l = ipd (π j) by force
    hence lm: l < m using nipdj by (metis le_eq_less_or_eq)
    have npd: ¬ ipd (π k) pd→ π l by (metis ipd(1) lipd nipdj pd pd_antisym)
    have nd: π l  nodes using path path_nodes by simp
    from no_pd_path[OF nd npd]
    obtain π' n where path': is_path π' and π'0: π' 0 = π l and π'n: π' n = return and nipd:  kan. π' ka  ipd (π k) .
    let  = (π@⇗lπ') « k
    have path'': is_path  by (metis π'0 path path' path_cons path_path_shift)
    moreover
    have kl: k < l using lipd cdj jl unfolding is_cdi_def by fastforce    
    have  0 = π k using kl by auto
    moreover
    have  (l + n - k) = return using π'n π'0 kl by auto
    moreover
    have ipd (π k) pd→ π k by (metis is_ipd_def ipd_is_ipd nretj path path_nodes)
    ultimately
    obtain l' where l': l'  (l + n - k)  l' = ipd (π k) unfolding is_pd_def by blast
    show False proof (cases )
      assume *: k + l'  l
      hence π (k + l') = ipd (π k) using l' by auto
      moreover 
      have k + l' < m by (metis "*" dual_order.strict_trans2 lm)
      ultimately
      show False using ipd(2) by simp
    next
      assume ¬ k + l'  l
      hence π' (k + l' - l) = ipd (π k) using l' by auto
      moreover
      have k + l' - l  n using l' kl by linarith  
      ultimately 
      show False using nipd by auto
    qed
  qed
qed

lemma ipd_icd_greatest_cd_not_ipd: assumes ipd: π m = ipd (π k)  n  {k..<m}. π n  ipd (π k)
and km: k < m and icdj: m icd⇗π⇖→ j shows j = (GREATEST j. k cd⇗π⇖→ j  ipd (π j)  π m)
proof -
  let ?j = GREATEST j. k cd⇗π⇖→ j  ipd (π j)  π m
  have kcdj: k cd⇗π⇖→ j using assms cd_ipd_is_cd is_icdi_def by blast   
  have nipd: ipd (π j)  π m using icdj unfolding is_icdi_def is_cdi_def by auto
  have bound:  j. k cd⇗π⇖→ j  ipd (π j)  π m  j  k unfolding is_cdi_def by simp
  have exists: k cd⇗π⇖→ j  ipd (π j)  π m (is ?P j) using kcdj nipd by auto
  note GreatestI_nat[of ?P _ k, OF exists] Greatest_le_nat[of ?P j k, OF exists]
  hence kcdj': k cd⇗π⇖→ ?j and ipd': ipd (π ?j)  π m and jj: j  ?j using bound by auto
  hence mcdj': m cd⇗π⇖→ ?j using ipd km cd_is_cd_ipd by auto
  show j = ?j proof (rule ccontr)
    assume j  ?j
    hence jlj: j < ?j using jj by simp
    moreover 
    have ?j < m using kcdj' km unfolding is_cdi_def by auto
    ultimately
    show False using icdj mcdj' unfolding is_icdi_def by auto
  qed
qed

lemma cd_impl_icd_cd: assumes i cd⇗π⇖→ l and i icd⇗π⇖→ k and ¬ i icd⇗π⇖→ l shows k cd⇗π⇖→ l
  using assms cd_split icd_uniq by metis

lemma cdi_is_cd_icdi: assumes k icd⇗π⇖→ j shows k cd⇗π⇖→ i  j cd⇗π⇖→ i  i = j 
  by (metis assms cd_impl_icd_cd cd_trans icd_imp_cd icd_uniq)

lemma same_ipd_stable: assumes k cd⇗π⇖→ i k cd⇗π⇖→ j i<j ipd (π i) = ipd (π k) shows ipd (π j) = ipd (π k)
proof -
  have jcdi: j cd⇗π⇖→ i by (metis is_cdi_def assms(1,2,3) cr_wn' le_antisym less_imp_le_nat)
  have 1: ipd (π j) pd→ π k by (metis assms(2) ipd_pd_cd)
  have 2: ipd (π k) pd→ π j by (metis assms(4) ipd_pd_cd jcdi)
  have 3: ipd (π k) pd→ (ipd (π j))  by (metis 2 IFC_def.is_cdi_def assms(1,2,4) atLeastAtMost_iff jcdi less_imp_le pd_node2 pd_pd_ipd) 
  have 4: ipd (π j) pd→ (ipd (π k)) by (metis 1 2 IFC_def.is_ipd_def assms(2) cd_not_pd ipd_is_ipd jcdi pd_node2 ret_no_cd) 
  show ?thesis using 3 4 pd_antisym by simp
qed

lemma icd_pd_intermediate': assumes icd: i icd⇗π⇖→ k  and j: k < j j < i shows π i pd→ (π j)
using j proof (induction i - j arbitrary: j rule: less_induct)
  case (less j)
  have ¬ i cd⇗π⇖→ j using less.prems icd unfolding is_icdi_def by force
  moreover 
  have is_path π using icd by (metis is_icdi_def)
  moreover 
  have π i  return using icd by (metis is_icdi_def ret_no_cd)
  ultimately
  have  l. j  l  l  i  π l = ipd (π j) unfolding is_cdi_def using less.prems by auto
  then obtain l where l: j  l l  i π l = ipd (π j) by blast
  hence lpd: π l pd→ (π j) by (metis is_ipd_def π i  return is_path π ipd_is_ipd path_nodes term_path_stable)
  show ?case proof (cases)
    assume l = i
    thus ?case using lpd by auto
  next
    assume l  i
    hence l < i using l by simp
    moreover
    have j  l using l by (metis is_ipd_def π i  return is_path π ipd_is_ipd path_nodes term_path_stable)
    hence j < l using l by simp
    moreover 
    hence i - l < i - j by (metis diff_less_mono2 less.prems(2))
    moreover
    have k < l by (metis l(1) less.prems(1) linorder_neqE_nat not_le order.strict_trans)
    ultimately
    have π i pd→ (π l) using less.hyps by auto
    thus ?case using lpd by (metis pd_trans)
  qed
qed

lemma icd_pd_intermediate: assumes icd: i icd⇗π⇖→ k  and j: k < j j  i shows π i pd→ (π j) 
using assms icd_pd_intermediate'[OF assms(1,2)] apply (cases j < i,metis) by (metis is_icdi_def le_neq_trans path_nodes pd_refl)

lemma no_icd_pd: assumes path: is_path π and noicd:  ln. ¬ k icd⇗π⇖→ l and nk: n  k shows π k pd→ π n
proof cases
  assume π k = return thus ?thesis by (metis path path_nodes return_pd)  
next
  assume nret: π k  return
  have nocd:  l. nl  ¬ k cd⇗π⇖→ l proof 
    fix l assume kcd: k cd⇗π⇖→ l and nl: n  l
    hence (k - n) cd⇗π«n⇖→ (l - n) using cd_path_shift[OF nl path] by simp
    hence  l. (k - n) icd⇗π«n⇖→ l using excd_impl_exicd by blast
    then obtain l' where "k - n icd⇗π « n⇖→ l'" ..
    hence k icd⇗π⇖→ (l' + n) using icd_path_shift[of n l' + n π k] path by auto
    thus False using noicd by auto
  qed    
  hence l. n  l  l<k   j  {l..k}. π j = ipd (π l) using path nret unfolding is_cdi_def by auto 
  thus ?thesis using nk proof (induction k - n arbitrary: n rule: less_induct,cases)
    case (less n) 
    assume n = k
    thus ?case using pd_refl path path_nodes by auto
  next
    case (less n)
    assume n  k
    hence nk: n < k using less(3) by auto
    with less(2) obtain j where jnk: j  {n..k} and ipdj: π j = ipd (π n) by blast
    have nretn: π n  return using nk nret term_path_stable path by auto
    with ipd_is_ipd path path_nodes is_ipd_def ipdj
    have jpdn: π j pd→ π n by auto
    show ?case proof cases
      assume j = k thus ?case using jpdn by simp
    next
      assume j  k
      hence jk: j < k using jnk by auto
      have j  n using ipdj by (metis ipd_not_self nretn path path_nodes)
      hence nj: n < j using jnk by auto
      have *: k - j < k - n using jk nj by auto
      
      with less(1)[OF *] less(2) jk nj
      have π k pd→ π j by auto

      thus ?thesis using jpdn pd_trans by metis
    qed
  qed
qed


lemma first_pd_no_cd: assumes path: is_path π and pd: π n pd→ π 0 and first:  l < n. π l  π n shows  l. ¬ n cd⇗π⇖→ l 
proof (rule ccontr, goal_cases)
  case 1
  then obtain l where ncdl: n cd⇗π⇖→ l by blast
  hence ln: l < n using is_cdi_def by auto
  have ¬ π n pd→ π l using ncdl cd_not_pd by (metis ln first)
  then obtain π' n' where path': is_path π' and π0: π' 0 = π l and πn: π' n' = return and notπn:  j n'. π' j  π n unfolding is_pd_def using path path_nodes by auto
  let  = π@⇗lπ'
  
  have is_path  by (metis π0 path path' path_cons)
  moreover
  have  0 = π 0 by auto
  moreover
  have  (n' + l) = return using π0 πn by auto
  ultimately
  obtain j where j: j  n' + l and jn:  j = π n using pd unfolding is_pd_def by blast
  show False proof cases
    assume j  l thus False using jn first ln by auto
  next
    assume ¬ j  l thus False using j jn notπn by auto
  qed
qed

lemma first_pd_no_icd: assumes path: is_path π and pd: π n pd→ π 0 and first:  l < n. π l  π n shows  l. ¬ n icd⇗π⇖→ l
  by (metis first first_pd_no_cd icd_imp_cd path pd)

lemma path_nret_ex_nipd: assumes is_path π  i. π i  return shows  i. ( ji. ( k>j. π k  ipd (π j))) proof(rule, rule ccontr)
  fix i
  assume ¬ (ji.  k>j. π k  ipd (π j))
  hence *:  ji. (k>j. π k = ipd (π j)) by blast
  have  j. (k>j. (π«i) k = ipd ((π«i) j)) proof
    fix j
    have i + j  i by auto
    then obtain k where k: k>i+j π k = ipd (π (i+j)) using * by blast
    hence (π«i) (k - i) = ipd ((π«i) j) by auto
    moreover  
    have k - i > j using k by auto
    ultimately
    show k>j. (π«i) k = ipd ((π«i) j) by auto
  qed
  moreover
  have is_path (π«i) using assms(1) path_path_shift by simp
  ultimately
  obtain k where (π«i) k = return using all_ipd_imp_ret by blast
  thus False using assms(2) by auto
qed

lemma path_nret_ex_all_cd: assumes is_path π  i. π i  return shows  i. ( ji. ( k>j. k cd⇗π⇖→ j))
unfolding is_cdi_def using assms path_nret_ex_nipd[OF assms] by (metis atLeastAtMost_iff ipd_not_self linorder_neqE_nat not_le path_nodes)


lemma path_nret_inf_all_cd: assumes is_path π  i. π i  return shows ¬ finite {j.  k>j. k cd⇗π⇖→ j} 
using unbounded_nat_set_infinite path_nret_ex_all_cd[OF assms] by auto

lemma path_nret_inf_icd_seq: assumes path: is_path π and nret:  i. π i  return 
obtains f where  i. f (Suc i) icd⇗π⇖→ f i range f = {i.  j>i. j cd⇗π⇖→ i} ¬ (i. f 0 cd⇗π⇖→ i)
proof -
  note path_nret_inf_all_cd[OF assms]
  then obtain f where ran: range f = {j.  k>j. k cd⇗π⇖→ j} and asc:  i. f i < f (Suc i) using infinite_ascending by blast
  have mono:  i j. i < j  f i < f j using asc by (metis lift_Suc_mono_less)
  {
    fix i
    have cd: f (Suc i) cd⇗π⇖→ f i using ran asc by auto
    have f (Suc i) icd⇗π⇖→ f i proof (rule ccontr)
      assume ¬ f (Suc i) icd⇗π⇖→ f i
      then obtain m where  im: f i < m and mi: m < f (Suc i) and cdm: f (Suc i) cd⇗π⇖→ m unfolding is_icdi_def using assms(1) cd by auto
      have  k>m. k cd⇗π⇖→m proof (rule,rule,cases)
        fix k assume f (Suc i) < k
        hence k cd⇗π⇖→ f (Suc i) using ran by auto
        thus k cd⇗π⇖→ m using cdm cd_trans by metis
      next
        fix k assume mk: m < k and ¬ f (Suc i) < k
        hence ik: k  f (Suc i) by simp
        thus k cd⇗π⇖→ m using cdm by (metis cdi_prefix mk)
      qed
      hence m  range f using ran by blast
      then obtain j where m: m = f j by blast
      show False using im mi mono unfolding m by (metis Suc_lessI le_less not_le)
    qed
  }
  moreover  
  {
    fix m
    assume cdm: f 0 cd⇗π⇖→ m
    have  k>m. k cd⇗π⇖→m proof (rule,rule,cases)
      fix k assume f 0 < k
      hence k cd⇗π⇖→ f 0 using ran by auto
      thus k cd⇗π⇖→ m using cdm cd_trans by metis
    next
      fix k assume mk: m < k and ¬ f 0 < k
      hence ik: k  f 0 by simp
      thus k cd⇗π⇖→ m using cdm by (metis cdi_prefix mk)
    qed
    hence m  range f using ran by blast
    then obtain j where m: m = f j by blast
    hence fj0: f j < f 0  using cdm m is_cdi_def by auto
    hence 0 < j by (metis less_irrefl neq0_conv)
    hence False using fj0 mono by fastforce
  }
  ultimately show thesis using that ran by blast
qed

lemma cdi_iff_no_strict_pd: i cd⇗π⇖→ k  is_path π  k < i  π i  return  ( j  {k..i}. ¬ (π k, π j)  pdt)
proof
  assume cd:i cd⇗π⇖→ k
  have 1: is_path π  k < i  π i  return using cd unfolding is_cdi_def by auto
  have 2:  j  {k..i}. ¬ (π k, π j)  pdt proof (rule ccontr)
    assume ¬ (j{k..i}. (π k, π j)  pdt)
    then obtain j where j  {k..i} and (π k, π j)  pdt by auto
    hence π j  π k and π j pd→ π k unfolding pdt_def by auto
    thus False using path_pd_ipd by (metis j  {k..i} atLeastAtMost_iff cd cd_not_pd cdi_prefix le_eq_less_or_eq) 
  qed
  show is_path π  k < i  π i  return  ( j  {k..i}. ¬ (π k, π j)  pdt) using 1 2 by simp
next
  assume is_path π  k < i  π i  return  ( j  {k..i}. ¬ (π k, π j)  pdt)
  thus i cd⇗π⇖→ k by (metis ipd_in_pdt term_path_stable less_or_eq_imp_le not_cd_impl_ipd path_nodes)
qed


subsection ‹Facts about Control Slices›

lemma last_cs: last (cs⇗πi) = π i by auto

lemma cs_not_nil: ‹cs⇗πn  [] by (auto)

lemma cs_return: assumes π n = return shows ‹cs⇗πn = [π n] by (metis assms cs.elims icd_imp_cd ret_no_cd)

lemma cs_0[simp]: ‹cs⇗π0 = [π 0] using is_icdi_def is_cdi_def by auto

lemma cs_inj: assumes is_path π π n  return ‹cs⇗πn = cs⇗πn' shows n = n' 
using assms proof (induction ‹cs⇗πn arbitrary: π n n' rule:rev_induct)
  case Nil hence False using cs_not_nil by metis thus ?case by simp
next
  case (snoc x xs π n n') show ?case proof (cases xs)
  case Nil 
  hence *: ¬ ( k. n icd⇗π⇖→k) using snoc(2) cs_not_nil 
    by (auto,metis append1_eq_conv append_Nil cs_not_nil)
  moreover
  have [x] = cs⇗πn' using Nil snoc by auto
  hence **: ¬ ( k. n' icd⇗π⇖→k) using cs_not_nil
    by (auto,metis append1_eq_conv append_Nil cs_not_nil)
  ultimately
  have  k. ¬ n cd⇗π⇖→ k  k. ¬ n' cd⇗π⇖→ k using excd_impl_exicd by auto blast+
  moreover 
  hence  π n = π n' using snoc(5,2) by auto (metis * ** list.inject)
  ultimately
  show n = n' using other_claim' snoc by blast
next
  case (Cons y ys)
  hence *:  k. n icd⇗π⇖→k using snoc(2) by auto (metis append_is_Nil_conv list.distinct(1) list.inject)
  then obtain k where k: n icd⇗π⇖→k by auto
  have k = (THE k . n icd⇗π⇖→ k) using k by (metis icd_is_the_icd)
  hence xsk: xs = cs⇗πk using * k snoc(2) unfolding cs.simps[of π n] by auto
  have **:  k. n' icd⇗π⇖→k using snoc(2)[unfolded snoc(5)] by auto (metis Cons append1_eq_conv append_Nil list.distinct(1))
  then obtain k' where k': n' icd⇗π⇖→ k' by auto
  hence k' = (THE k . n' icd⇗π⇖→ k) using k' by (metis icd_is_the_icd)
  hence xsk': xs = cs⇗πk' using ** k' snoc(5,2) unfolding cs.simps[of π n'] by auto
  hence ‹cs⇗πk = cs⇗πk' using xsk by simp
  moreover
  have kn: k < n using k by (metis is_icdi_def is_cdi_def)
  hence π k  return using snoc by (metis term_path_stable less_imp_le)
  ultimately
  have kk'[simp]: k' = k using snoc(1) xsk snoc(3) by metis
  have nk0: n - k icd⇗π«k⇖→ 0 n' - k icd⇗π«k⇖→ 0 using k k' icd_path_shift0 snoc(3) by auto
  moreover 
  have nkr: (π«k)(n-k)  return using snoc(4) kn by auto
  moreover 
  have is_path (π«k) by (metis path_path_shift snoc.prems(1))
  moreover 
  have kn': k < n' using k' kk' by (metis is_icdi_def is_cdi_def)
  have π n = π n' using snoc(5) * ** by auto
  hence (π«k)(n-k) = (π«k)(n'-k) using kn kn' by auto 
  ultimately  
  have n - k = n' - k using other_claim  by auto
  thus n = n' using kn kn' by auto
qed
qed

lemma cs_cases: fixes π i 
obtains (base) ‹cs⇗πi = [π i] and  k. ¬ i cd⇗π⇖→ k | 
(depend) k where  ‹cs⇗πi = (cs⇗πk)@[π i] and i icd⇗π⇖→ k 
proof cases
  assume *:  k. i icd⇗π⇖→ k
  then obtain k where k: i icd⇗π⇖→ k ..
  hence k = (THE k. i icd⇗π⇖→ k)  by (metis icd_is_the_icd)
  hence ‹cs⇗πi = (cs⇗πk)@[π i] using * by auto
  with k that show thesis by simp
next
  assume *: ¬ ( k. i icd⇗π⇖→ k)
  hence  k. ¬ i cd⇗π⇖→ k by (metis excd_impl_exicd)
  moreover 
  have ‹cs⇗πi = [π i] using * by auto
  ultimately
  show thesis using that by simp
qed

lemma cs_length_one: assumes length (cs⇗πi) = 1 shows  ‹cs⇗πi = [π i] and  k. ¬ i cd⇗π⇖→ k
  apply (cases i π rule: cs_cases)
  using assms cs_not_nil 
    apply auto 
  apply (cases i π rule: cs_cases) 
  using assms cs_not_nil 
  by auto

lemma cs_length_g_one: assumes length (cs⇗πi)  1 obtains k where  ‹cs⇗πi = (cs⇗πk)@[π i] and i icd⇗π⇖→ k 
  apply (cases i π rule: cs_cases) 
  using assms cs_not_nil by auto

lemma claim: assumes  path: is_path π is_path π' and  ii: ‹cs⇗πi = cs⇗π'i' and jj: ‹cs⇗πj = cs⇗π'j' 
and bl: butlast (cs⇗πi) = butlast (cs⇗πj) and nret: π i  return and ilj: i < j 
shows i' < j'
proof (cases )
  assume *: length (cs⇗πi) = 1
  hence **: length (cs⇗πi) = 1 length (cs⇗πj) = 1 length (cs⇗π'i') = 1 length (cs⇗π'j') = 1  
    apply metis
    apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil) 
    apply (metis "*" ii)
    by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
  then obtain ‹cs⇗πi = [π i] ‹cs⇗πj = [π j] ‹cs⇗π'j' = [π' j'] ‹cs⇗π'i'= [π' i'] 
     k. ¬ j cd⇗π⇖→ k  k. ¬ i' cd⇗π'⇖→ k  k. ¬ j' cd⇗π'⇖→ k
  by (metis cs_length_one ** )
  moreover 
  hence π i = π' i' π j = π' j' using  assms by auto
  ultimately
  show i' < j' using nret ilj path claim'' by blast
next
  assume *: length (cs⇗πi)  1
  hence **: length (cs⇗πi)  1 length (cs⇗πj)  1 length (cs⇗π'i')  1 length (cs⇗π'j')  1  
    apply metis
    apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil)
    apply (metis "*" ii)
    by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
  obtain k l k' l' where ***:
    ‹cs⇗πi = (cs⇗πk)@[π i] ‹cs⇗πj = (cs⇗πl)@[π j]  ‹cs⇗π'i' = (cs⇗π'k')@[π' i'] ‹cs⇗π'j' = (cs⇗π'l')@[π' j'] and
    icds: i icd⇗π⇖→ k j icd⇗π⇖→ l i' icd⇗π'⇖→ k' j' icd⇗π'⇖→ l'
    by (metis ** cs_length_g_one)
  hence ‹cs⇗πk = cs⇗πl ‹cs⇗π'k' = cs⇗π'l' using assms by auto
  moreover
  have π k  return π' k'  return using nret 
    apply (metis is_icdi_def icds(1) is_cdi_def term_path_stable less_imp_le) 
    by (metis is_cdi_def is_icdi_def icds(3) term_path_stable less_imp_le)
  ultimately  
  have lk[simp]: l = k l' = k' using path cs_inj by auto
  let  = π « k 
  let ?π' = π'«k'
  have i-k icd⇗⇖→ 0 j-k icd⇗⇖→ 0 i'-k' icd⇗?π'⇖→ 0 j'-k' icd⇗?π'⇖→ 0 using icd_path_shift0 path icds by auto
  moreover
  have ki: k < i using icds by (metis is_icdi_def is_cdi_def)
  hence i-k < j-k by (metis diff_is_0_eq diff_less_mono ilj nat_le_linear order.strict_trans)
  moreover
  have πi: π i = π' i' π j = π' j' using assms *** by auto
  have k' < i' k' < j' using icds unfolding lk by (metis is_cdi_def is_icdi_def)+ 
  hence  (i-k) = ?π' (i'-k')  (j-k) = ?π' (j'-k') using πi ki ilj by auto
  moreover 
  have  (i-k)  return using nret ki by auto
  moreover
  have is_path  is_path ?π' using path path_path_shift by auto
  ultimately
  have i'-k' < j' - k' using claim' by blast
  thus i' < j' by (metis diff_is_0_eq diff_less_mono less_nat_zero_code linorder_neqE_nat nat_le_linear)
qed

lemma cs_split': assumes ‹cs⇗πi = xs@[x,x']@ys  shows  m. cs⇗πm = xs@[x]  i cd⇗π⇖→ m 
using assms proof (induction ys arbitrary: i rule:rev_induct ) 
  case (snoc y ys)
  hence length (cs⇗πi)  1 by auto
  then obtain i' where ‹cs⇗πi = (cs⇗πi') @ [π i] and *: i icd⇗π⇖→ i' using cs_length_g_one[of π i] by metis
  hence ‹cs⇗πi' = xs@[x,x']@ys using snoc(2) by (metis append1_eq_conv append_assoc)
  then obtain m where **: ‹cs⇗πm = xs @ [x] and i' cd⇗π⇖→ m using snoc(1) by blast
  hence i cd⇗π⇖→ m using * cd_trans by (metis is_icdi_def)
  with ** show ?case by blast
next
  case Nil
  hence length (cs⇗πi)  1 by auto
  then obtain i' where a: ‹cs⇗πi = (cs⇗πi') @ [π i] and *: i icd⇗π⇖→ i' using cs_length_g_one[of π i] by metis
  have ‹cs⇗πi = (xs@[x])@[x'] using Nil by auto
  hence ‹cs⇗πi' = xs@[x] using append1_eq_conv a by metis  
  thus ?case using * unfolding is_icdi_def by blast
qed

lemma cs_split: assumes ‹cs⇗πi = xs@[x]@ys@[π i]  shows  m. cs⇗πm = xs@[x]  i cd⇗π⇖→ m proof -
  obtain x' ys' where ys@[π i] = [x']@ys' by (metis append_Cons append_Nil neq_Nil_conv)
  thus ?thesis using cs_split'[of π i xs x x' ys'] assms by auto
qed

lemma cs_less_split: assumes xs  ys obtains a as where ys = xs@a#as
  using assms unfolding cs_less.simps apply auto
by (metis Cons_nth_drop_Suc append_take_drop_id)

lemma cs_select_is_cs: assumes is_path π xs  Nil xs  cs⇗πk shows ‹cs⇗π(π¡xs) = xs k cd⇗π⇖→ (π¡xs)proof -
  obtain b bs where b: ‹cs⇗πk = xs@b#bs using assms cs_less_split by blast
  obtain a as where a: xs = as@[a] using assms by (metis rev_exhaust)
  have ‹cs⇗πk = as@[a,b]@bs using a b by auto
  then obtain k' where csk: ‹cs⇗πk' = xs and is_cd: k cd⇗π⇖→ k' using cs_split' a by blast
  hence nret: π k'  return by (metis is_cdi_def term_path_stable less_imp_le)
  show a: ‹cs⇗π(π¡xs) = xs unfolding cs_select_def using cs_inj[OF assms(1) nret] csk the_equality[of _ k']
    by (metis (mono_tags))
  show k cd⇗π⇖→ (π¡xs) unfolding cs_select_def by (metis a assms(1) cs_inj cs_select_def csk is_cd nret)
qed

lemma cd_in_cs: assumes n cd⇗π⇖→ m shows  ns. cs⇗πn = (cs⇗πm) @ ns @[π n] 
using assms proof (induction rule: cd_induct)
  case (base  n) thus ?case by (metis append_Nil cs.simps icd_is_the_icd)
next
  case (IS k n)
  hence ‹cs⇗πn = cs⇗πk @ [π n] by (metis cs.simps icd_is_the_icd)  
  thus ?case using IS by force
qed

lemma butlast_cs_not_cd: assumes butlast (cs⇗πm) = butlast (cs⇗πn) shows ¬ m cd⇗π⇖→n
by (metis append_Cons append_Nil append_assoc assms cd_in_cs cs_not_nil list.distinct(1) self_append_conv snoc_eq_iff_butlast)

lemma wn_cs_butlast: assumes butlast (cs⇗πm) = butlast (cs⇗πn) i cd⇗π⇖→ m j cd⇗π⇖→ n m<n shows i<j
proof (rule ccontr)
  assume ¬ i < j
  moreover
  have ¬ n cd⇗π⇖→ m by (metis assms(1) butlast_cs_not_cd)
  ultimately
  have n  m using assms(2,3) cr_wn'' by auto
  thus False using assms(4) by auto
qed


text ‹This is the central theorem making the control slice suitable for matching indices between executions.›

theorem cs_order: assumes path: is_path π is_path π' and csi: ‹cs⇗πi = cs⇗π'i' 
and csj: ‹cs⇗πj = cs⇗π'j' and nret: π i  return and ilj: i < j   
shows i'<j'
proof -
  have ‹cs⇗πi  cs⇗πj using cs_inj[OF path(1) nret] ilj by blast
  moreover 
  have ‹cs⇗πi  Nil ‹cs⇗πj  Nil by (metis cs_not_nil)+
  ultimately show ?thesis proof (cases rule: list_neq_prefix_cases)
    case (diverge xs x x' ys ys')
    note csx = ‹cs⇗πi = xs @ [x] @ ys
    note csx' = ‹cs⇗πj = xs @ [x'] @ ys'
    note xx = x  x'
    show i' < j' proof (cases ys) 
      assume ys: ys = Nil
      show ?thesis proof (cases ys')
        assume ys': ys' = Nil
        have cs: ‹cs⇗πi = xs @ [x] ‹cs⇗πj = xs @ [x'] by (metis append_Nil2 csx ys, metis append_Nil2 csx' ys')
        hence bl: butlast (cs⇗πi) = butlast (cs⇗πj) by auto        
        show i' < j' using claim[OF path csi csj bl nret ilj] .
      next
        fix y' zs'
        assume ys': ys' = y'#zs'
        have cs: ‹cs⇗πi = xs @ [x] ‹cs⇗πj = xs @ [x',y']@ zs' by (metis append_Nil2 csx ys, metis append_Cons append_Nil csx' ys')         
        obtain n where n: ‹cs⇗πn = xs@[x'] and jn: j cd⇗π⇖→ n using cs cs_split' by blast
        obtain n' where n': ‹cs⇗π'n' = xs@[x'] and jn': j' cd⇗π'⇖→ n' using cs cs_split' unfolding csj by blast
        have csn : ‹cs⇗πn = cs⇗π'n' and bl: butlast (cs⇗πi) = butlast (cs⇗πn) using n n' cs by auto
        hence bl': butlast (cs⇗π'i') = butlast (cs⇗π'n') using csi by auto
        have notcd: ¬ i cd⇗π⇖→ n by (metis butlast_cs_not_cd bl)
        have nin: i  n using cs n xx by auto
        have iln: i < n apply (rule ccontr) using cr_wn'[OF jn notcd] nin ilj by auto
        note claim[OF path csi csn bl nret iln]
        hence i' < n' .
        thus i' < j' using jn' unfolding is_cdi_def by auto
      qed
    next
      fix y zs
      assume ys: ys = y#zs
      show ?thesis proof (cases ys')
        assume ys' : ys' = Nil
        have cs: ‹cs⇗πi = xs @ [x,y]@zs ‹cs⇗πj = xs @ [x'] by (metis append_Cons append_Nil csx ys, metis append_Nil2 csx' ys')
        obtain n where n: ‹cs⇗πn = xs@[x] and jn: i cd⇗π⇖→ n using cs cs_split' by blast
        obtain n' where n': ‹cs⇗π'n' = xs@[x] and jn': i' cd⇗π'⇖→ n' using cs cs_split' unfolding csi by blast
        have csn : ‹cs⇗πn = cs⇗π'n' and bl: butlast (cs⇗πn) = butlast (cs⇗πj) using n n' cs by auto
        hence bl': butlast (cs⇗π'j') = butlast (cs⇗π'n') using csj by auto
        have notcd: ¬ j' cd⇗π'⇖→ n' by (metis butlast_cs_not_cd bl')
        have nin: n < i using jn unfolding is_cdi_def by auto
        have nlj: n < j using nin ilj by auto
        note claim[OF path csn csj bl _ nlj]
        hence nj': n' < j' using term_path_stable[OF path(1) _] less_imp_le nin nret by auto
        show i' < j' apply(rule ccontr) using cdi_prefix[OF jn' nj'] notcd by auto
      next
        fix y' zs'
        assume ys' : ys' = y'#zs'
        have cs: ‹cs⇗πi = xs@[x,y]@zs ‹cs⇗πj = xs@[x',y']@zs' by (metis append_Cons append_Nil csx ys,metis append_Cons append_Nil csx' ys')
        have neq: ‹cs⇗πi  cs⇗πj using cs_inj path nret ilj by blast
        obtain m where m: ‹cs⇗πm = xs@[x] and im: i cd⇗π⇖→ m using cs cs_split' by blast
        obtain n where n: ‹cs⇗πn = xs@[x'] and jn: j cd⇗π⇖→ n using cs cs_split' by blast
        obtain m' where m': ‹cs⇗π'm' = xs@[x] and im': i' cd⇗π'⇖→ m' using cs cs_split' unfolding csi by blast
        obtain n' where n': ‹cs⇗π'n' = xs@[x'] and jn': j' cd⇗π'⇖→ n' using cs cs_split' unfolding csj by blast
        have m  n using ilj m n wn_cs_butlast[OF _ jn im] by force
        moreover
        have m  n using m n xx by (metis last_snoc)
        ultimately 
        have mn: m < n by auto
        moreover 
        have π m  return by (metis last_cs last_snoc m mn n path(1) term_path_stable xx less_imp_le)
        moreover  
        have butlast (cs⇗πm) = butlast (cs⇗πn) ‹cs⇗πm = cs⇗π'm' ‹cs⇗πn = cs⇗π'n' using m n n' m' by auto
        ultimately
        have m' < n' using claim path by blast
        thus i' < j' using m' n' im' jn' wn_cs_butlast by (metis butlast_snoc)        
      qed
    qed
  next
    case (prefix1 xs)
    note pfx = ‹cs⇗πi = cs⇗πj @ xs
    note xs = xs  []
    obtain a as where xs = a#as using xs by (metis list.exhaust)
    moreover
    obtain bs b where bj: ‹cs⇗πj = bs@[b] using cs_not_nil by (metis rev_exhaust)
    ultimately
    have ‹cs⇗πi = bs@[b,a]@as using pfx by auto
    then obtain m where ‹cs⇗πm = bs@[b] and cdep:  i cd⇗π⇖→ m using cs_split' by blast
    hence mi: m = j using bj cs_inj by (metis is_cdi_def term_path_stable less_imp_le)
    hence i cd⇗π⇖→ j using cdep by auto
    hence False using ilj unfolding is_cdi_def by auto
    thus i' < j' ..
  next
    case (prefix2 xs)
    have pfx : ‹cs⇗π'i' @ xs = cs⇗π'j' using prefix2 csi csj by auto
    note xs = xs  []
     obtain a as where xs = a#as using xs by (metis list.exhaust)
    moreover
    obtain bs b where bj: ‹cs⇗π'i'  = bs@[b] using cs_not_nil by (metis rev_exhaust)
    ultimately
    have ‹cs⇗π'j' = bs@[b,a]@as using pfx by auto
    then obtain m where ‹cs⇗π'm = bs@[b] and cdep:  j' cd⇗π'⇖→ m using cs_split' by blast
    hence mi: m = i' using bj cs_inj by (metis is_cdi_def term_path_stable less_imp_le)
    hence j' cd⇗π'⇖→ i' using cdep by auto
    thus i' < j' unfolding is_cdi_def by auto  
  qed
qed

lemma cs_order_le: assumes path: is_path π is_path π' and csi: ‹cs⇗πi = cs⇗π'i' 
and csj: ‹cs⇗πj = cs⇗π'j' and nret: π i  return and ilj: i  j   
shows i'j' proof cases
  assume i < j with cs_order[OF assms(1,2,3,4,5)] show ?thesis by simp
next
  assume ¬ i < j
  hence i = j using ilj by simp
  hence csij: ‹cs⇗π'i' = cs⇗π'j' using csi csj by simp  
  have nret': π' i'  return using nret last_cs csi by metis
  show ?thesis using cs_inj[OF path(2) nret' csij] by simp
qed

lemmas cs_induct[case_names cs] = cs.induct

lemma icdi_path_swap: assumes is_path π' j icd⇗π⇖→k π =⇘jπ' shows j icd⇗π'⇖→k using assms unfolding eq_up_to_def is_icdi_def is_cdi_def by auto

lemma icdi_path_swap_le: assumes is_path π' j icd⇗π⇖→k π =⇘nπ' j  n shows j icd⇗π'⇖→k by (metis assms icdi_path_swap eq_up_to_le)

lemma cs_path_swap: assumes is_path π is_path π' π =⇘kπ' shows ‹cs⇗πk = cs⇗π'k using assms(1,3) proof (induction π k rule:cs_induct,cases)
  case (cs π k)     
  let ?l = (THE l. k icd⇗π⇖→ l)
  assume *: l. k icd⇗π⇖→ l
  have kicd: k icd⇗π⇖→ ?l by (metis "*" icd_is_the_icd)
  hence ?l < k unfolding is_cdi_def[of k π ?l] is_icdi_def[of k π ?l] by auto
  hence  i?l. π i = π' i using cs(2,3) unfolding eq_up_to_def by auto
  hence csl: ‹cs⇗π?l = cs⇗π'?l using cs(1,2) * unfolding eq_up_to_def by auto 
  have kicd: k icd⇗π⇖→ ?l by (metis "*" icd_is_the_icd)
  hence csk: ‹cs⇗πk = cs⇗π?l @ [π k] using kicd by auto
  have kicd': k icd⇗π'⇖→ ?l using kicd icdi_path_swap[OF assms(2) _ cs(3)] by simp
  hence ?l = (THE l. k icd⇗π'⇖→ l) by (metis icd_is_the_icd)
  hence csk': ‹cs⇗π'k = cs⇗π'?l @ [π' k] using kicd' by auto
  have π' k = π k using cs(3) unfolding eq_up_to_def by auto
  with csl csk csk'  
  show ?case by auto
next
  case (cs π k)
  assume *: ¬ (l. k icd⇗π⇖→ l)
  hence csk: ‹cs⇗πk = [π k] by auto
  have ¬ (l. k icd⇗π'⇖→ l) apply (rule ccontr) using * icdi_path_swap_le[OF cs(2) _, of k π'] cs(3) by (metis eq_up_to_sym le_refl)
  hence csk': ‹cs⇗π'k = [π' k] by auto
  with csk show ?case using cs(3) eq_up_to_apply by auto
qed

lemma cs_path_swap_le: assumes is_path π is_path π' π =⇘nπ' k  n shows ‹cs⇗πk = cs⇗π'k by (metis assms cs_path_swap eq_up_to_le)

lemma cs_path_swap_cd: assumes is_path π and is_path π' and ‹cs⇗πn = cs⇗π'n' and n cd⇗π⇖→ k 
obtains k' where n' cd⇗π'⇖→ k' and ‹cs⇗πk = cs⇗π'k'
proof -
  from cd_in_cs[OF assms(4)]
  obtain ns where *: ‹cs⇗πn = cs⇗πk @ ns @ [π n] by blast
  obtain xs x where csk: ‹cs⇗πk = xs @ [x] by (metis cs_not_nil rev_exhaust)
  have π n = π' n' using assms(3) last_cs by metis
  hence **: ‹cs⇗π'n' = xs@[x]@ns@[π' n'] using * assms(3) csk by auto
  from cs_split[OF **]
  obtain k' where ‹cs⇗π'k' = xs @ [x] n' cd⇗π'⇖→ k' by blast
  thus thesis using that csk by auto
qed

lemma path_ipd_swap: assumes is_path π π k  return k < n 
obtains π' m where is_path π' π =⇘nπ' k < m π' m = ipd (π' k)  l  {k..<m}. π' l  ipd (π' k)
proof -
  obtain π' r where *: π' 0 = π n is_path π' π' r = return by (metis assms(1) path_nodes reaching_ret)
  let  = π@⇗nπ'
  have path: is_path  and ret:  (n + r) = return and equpto:   =⇘nπ using assms path_cons * path_append_eq_up_to by auto
  have πk:  k = π k by (metis assms(3) less_imp_le_nat path_append_def)
  obtain j where j: k < j  j  (n + r)   j = ipd (π k) (is ?P j )by (metis πk assms(2) path path_ret_ipd ret)
  define m where m: m  LEAST m . ?P m
  have Pm: ?P m using LeastI[of ?P j] j m by auto
  hence km: k < m m  (n + r)  m = ipd (π k) by auto
  have le: l. ?P l  m  l using Least_le[of ?P] m by blast
  have πknipd:  k  ipd (π k) by (metis πk assms(1) assms(2) ipd_not_self path_nodes)
  have nipd': l. k < l  l < m   l  ipd (π k) apply (rule ccontr) using le km(2) by force
  have  l  {k..<m}.  l  ipd(π k) using πknipd nipd' by(auto, metis le_eq_less_or_eq,metis le_eq_less_or_eq)
  thus thesis using that by (metis πk eq_up_to_sym km(1) km(3) path path_append_eq_up_to)
qed

lemma cs_sorted_list_of_cd': ‹cs⇗πk = map π (sorted_list_of_set { i . k cd⇗π⇖→ i}) @ [π k] 
proof (induction π k rule: cs.induct, cases)
  case (1 π k)
  assume  j. k icd⇗π⇖→ j
  then obtain j where j: "k icd⇗π⇖→ j" ..
  hence csj: ‹cs⇗πj = map π (sorted_list_of_set {i. j cd⇗π⇖→ i}) @ [π j] by (metis "1.IH" icd_is_the_icd)
  have {i. k cd⇗π⇖→ i} = insert j {i. j cd⇗π⇖→ i} using cdi_is_cd_icdi[OF j] by auto
  moreover
  have f: finite {i. j cd⇗π⇖→ i} unfolding is_cdi_def by auto
  moreover
  have j  {i. j cd⇗π⇖→ i} unfolding is_cdi_def by auto
  ultimately
  have sorted_list_of_set { i . k cd⇗π⇖→ i} = insort j (sorted_list_of_set { i . j cd⇗π⇖→ i}) using sorted_list_of_set_insert by auto
  moreover
  have  x   {i. j cd⇗π⇖→ i}. x < j unfolding is_cdi_def by auto
  hence  x  set (sorted_list_of_set {i. j cd⇗π⇖→ i}). x < j by (simp add: f) 
  ultimately
  have sorted_list_of_set { i . k cd⇗π⇖→ i} = (sorted_list_of_set { i . j cd⇗π⇖→ i})@[j]  using insort_greater by auto
  hence ‹cs⇗πj = map π (sorted_list_of_set { i . k cd⇗π⇖→ i}) using csj by auto
  thus ?case by (metis icd_cs j)
next
  case (1 π k)
  assume *: ¬ ( j. k icd⇗π⇖→ j)
  hence ‹cs⇗πk = [π k] by (metis cs_cases)
  moreover 
  have { i . k cd⇗π⇖→ i} = {} by (auto, metis * excd_impl_exicd)
  ultimately 
  show ?case by (metis append_Nil list.simps(8) sorted_list_of_set_empty)
qed

lemma cs_sorted_list_of_cd: ‹cs⇗πk = map π (sorted_list_of_set ({ i . k cd⇗π⇖→ i}  {k})) proof -
  have le:  x  {i. k cd⇗π⇖→i}. y  {k}. x < y unfolding is_cdi_def by auto
  have fin: finite {i. k cd⇗π⇖→i} finite {k} unfolding is_cdi_def by auto  
  show ?thesis unfolding cs_sorted_list_of_cd'[of π k] sorted_list_of_set_append[OF fin le] by auto
qed

lemma cs_not_ipd: assumes k cd⇗π⇖→ j  ipd (π j)  ipd (π k) (is ?Q j)
shows ‹cs⇗π(GREATEST j. k cd⇗π⇖→ j  ipd (π j)  ipd (π k)) = [ncs⇗πk . ipd n  ipd (π k)]
(is ‹cs⇗π?j = filter ?P _) 
proof -  
  have csk: ‹cs⇗πk = map π (sorted_list_of_set ({ i . k cd⇗π⇖→ i }  {k})) by (metis cs_sorted_list_of_cd)
  have csj: ‹cs⇗π?j = map π (sorted_list_of_set ({i. ?j cd⇗π⇖→ i }  {?j})) by (metis cs_sorted_list_of_cd)
  
  have bound:  j. k cd⇗π⇖→ j  ipd (π j)  ipd(π k)  j  k unfolding is_cdi_def by simp
    
  have kcdj: k cd⇗π⇖→ ?j and ipd': ipd (π ?j)  ipd(π k) using GreatestI_nat[of ?Q j k, OF assms] bound by auto
   
  have greatest:  j. k cd⇗π⇖→ j  ipd (π j)  ipd (π k)  j  ?j using Greatest_le_nat[of ?Q  _ k] bound by auto
  have less_not_ipdk:  j. k cd⇗π⇖→ j  j < ?j  ipd (π j)  ipd (π k)   by (metis (lifting) ipd' kcdj same_ipd_stable)
  hence le_not_ipdk:  j. k cd⇗π⇖→ j  j  ?j  ipd (π j)  ipd (π k) using kcdj ipd' by (case_tac j = ?j,auto)
  have *: {j  {i. k cd⇗π⇖→i}  {k}. ?P (π j)} = insert ?j { i . ?j cd⇗π⇖→ i} 
    apply auto  
    apply (metis (lifting, no_types) greatest cr_wn'' kcdj le_antisym le_refl)
    apply (metis kcdj)
    apply (metis ipd')
    apply (metis (full_types) cd_trans kcdj)
    apply (subgoal_tac k cd⇗π⇖→ x)
    apply (metis (lifting, no_types) is_cdi_def less_not_ipdk)
    by (metis (full_types) cd_trans kcdj)
  have finite ({i . k cd⇗π⇖→ i}  {k}) unfolding is_cdi_def by auto
  note filter_sorted_list_of_set[OF this, of ?P o π]
  hence [ncs⇗πk . ipd n  ipd(π k)] = map π (sorted_list_of_set {j  {i. k cd⇗π⇖→i}  {k}. ?P (π j)}) unfolding csk filter_map by auto 
  also 
  have  =  map π (sorted_list_of_set (insert ?j { i . ?j cd⇗π⇖→ i})) unfolding * by auto
  also 
  have  = cs⇗π?j using csj by auto
  finally 
  show ?thesis by metis
qed

lemma cs_ipd: assumes ipd: π m = ipd (π k)  n  {k..<m}. π n  ipd (π k)
and km: k < m shows ‹cs⇗πm = [ncs⇗πk . ipd n  π m] @ [π m]
proof cases
  assume  j. m icd⇗π⇖→ j  
  then obtain j where jicd: m icd⇗π⇖→ j by blast
  hence *: ‹cs⇗πm = cs⇗πj @ [π m] by (metis icd_cs)
  have j: j = (GREATEST j. k cd⇗π⇖→ j  ipd (π j)  π m) using jicd assms ipd_icd_greatest_cd_not_ipd by blast
  moreover
  have ipd (π j)  ipd (π k) by (metis is_cdi_def is_icdi_def is_ipd_def cd_not_pd ipd(1) ipd_is_ipd jicd path_nodes less_imp_le term_path_stable)
  moreover
  have k cd⇗π⇖→ j unfolding j by (metis (lifting, no_types) assms(3) cd_ipd_is_cd icd_imp_cd ipd(1) ipd(2) j jicd)
  ultimately
  have ‹cs⇗πj = [ncs⇗πk . ipd n  π m] using cs_not_ipd[of k π j] ipd(1) by metis
  thus ?thesis using * by metis
next
  assume noicd: ¬ ( j. m icd⇗π⇖→ j)  
  hence csm: ‹cs⇗πm = [π m] by auto
  have j. k cd⇗π⇖→j  ipd(π j) = π m using cd_is_cd_ipd[OF km ipd] by (metis excd_impl_exicd noicd)
  hence *: {j  {i. k cd⇗π⇖→ i}  {k}. ipd (π j)  π m} = {} using ipd(1) by auto
  have **: ((λn. ipd n  π m) o π) = (λn. ipd (π n)  π m) by auto
  have fin: finite ({i. k cd⇗π⇖→ i}  {k}) unfolding is_cdi_def by auto
  note csk = cs_sorted_list_of_cd[of π k]
  hence [ncs⇗πk . ipd n  π m] = [n (map π (sorted_list_of_set ({i. k cd⇗π⇖→ i}  {k}))) . ipd n  π m] by simp
  also
  have  = map π [n <- sorted_list_of_set ({i. k cd⇗π⇖→ i}  {k}). ipd (π n)  π m]  by (auto simp add: filter_map **) 
  also 
  have  = [] unfolding * filter_sorted_list_of_set[OF fin, of λn. ipd (π n)  π m] by auto
  finally
  show ?thesis using csm by (metis append_Nil)
qed

lemma converged_ipd_same_icd: assumes path: is_path π is_path π' and  converge: l < m ‹cs⇗πm = cs⇗π'm' 
and csk: ‹cs⇗πk = cs⇗π'k' and icd: l icd⇗π⇖→ k and suc: π (Suc k) = π' (Suc k')
and ipd: π' m' = ipd (π k)  n  {k'..<m'}. π' n  ipd (π k)
shows l'. cs⇗πl = cs⇗π'l'
proof cases
  assume l: l = Suc k
  hence Suc k cd⇗π⇖→ k using icd by (metis is_icdi_def)
  hence π (Suc k)  ipd (π k) unfolding is_cdi_def by auto
  hence π' (Suc k')  ipd (π' k') by (metis csk last_cs suc)
  moreover 
  have π' (Suc k')  return by (metis Suc k cd⇗π⇖→ k ret_no_cd suc)
  ultimately
  have Suc k' cd⇗π'⇖→ k' unfolding is_cdi_def using path(2) apply auto 
  by (metis ipd_not_self le_Suc_eq le_antisym path_nodes term_path_stable)
  hence Suc k' icd⇗π'⇖→ k' unfolding is_icdi_def using path(2) by fastforce  
  hence ‹cs⇗π'(Suc k') = cs⇗π'k' @[π' (Suc k')] using icd_cs by auto 
  moreover
  have ‹cs⇗πl = cs⇗πk @ [π l] using icd icd_cs by auto
  ultimately 
  have ‹cs⇗πl = cs⇗π'(Suc k') by (metis csk l suc)
  thus ?thesis by blast
next
  assume nsuck: l  Suc k
  have kk'[simp]: π' k' = π k by (metis csk last_cs)
  have kl: k < l using icd unfolding is_icdi_def is_cdi_def by auto
  hence skl: Suc k < l by (metis Suc_lessI nsuck)
  hence lpd: π l pd→ π (Suc k) using icd icd_pd_intermediate by auto
  have km: k < m by (metis converge(1) kl order.strict_trans)  
  have lcd: l cd⇗π⇖→ k using icd is_icdi_def by auto
  hence ipdk_pdl: ipd (π k) pd→ (π l) by (metis ipd_pd_cd)
  have *: ipd (π k)  nodes by (metis ipdk_pdl pd_node1)
  have nretk: π k  return by (metis kl lcd path(1) ret_no_cd term_path_stable less_imp_le)
  have **: ¬ (π l) pd→ ipd (π k) proof 
    assume a: π l pd→ ipd (π k)
    hence π l pd→ (π k) by (metis is_ipd_def k < l ipd_is_ipd ipdk_pdl path(1) path_nodes pd_antisym term_path_stable less_imp_le)
    moreover 
    have π l  (π k) by (metis "*" a ipd_not_self ipdk_pdl lcd pd_antisym ret_no_cd)
    ultimately
    show False using lcd cd_not_pd by auto
  qed

  have km': k' < m' using cs_order[OF path csk converge(2) nretk km] . 

  obtain π'' n'' where path'': is_path π''  and π''0: π'' 0 = ipd (π k) and π''n: π'' n'' = return and notπl:  in''. π'' i  π l using no_pd_path[OF * **] .
  let ?π' = (π' @⇗m'π'') « Suc k'
  have is_path ?π' by (metis π''0 ipd(1) path'' path(2) path_cons path_path_shift)
  moreover 
  have ?π' 0 = π (Suc k) using km' suc by auto
  moreover
  have ?π' (m' - Suc k' + n'') = return using π''n km' π''0 ipd(1) by auto  
  ultimately
  obtain l'' where l'': l''  m' - Suc k' + n'' ?π' l'' = π l using lpd unfolding is_pd_def by blast
  have l''m: l''  m' - Suc k' apply (rule ccontr) using l'' notπl km' by (cases Suc (k' + l'')  m', auto)
  let ?l' = Suc ( k' + l'')
  have lm': ?l'  m' using l''m km' by auto
  
  ― ‹Now we have found our desired l'›
  have 1: π' ?l' = π l using  l'' l''m lm' by auto
  have 2: k' < ?l' by simp  
  have 3: ?l' < m' apply (rule ccontr) using lm' by (simp, metis "**" 1 ipd(1) ipdk_pdl)  
  
  ― ‹Need the least such l'›

  let ?P = λ l'. π' l' = π l  k' < l'  l' < m'

  have *: ?P ?l' using 1 2 3 by blast

  define l' where l': l' == LEAST l'. ?P l'
  
  have πl': π' l' = π l using l' 1 2 3 LeastI[of ?P] by blast  
  have kl': k' < l' using l' 1 2 3 LeastI[of ?P] by blast
  have lm': l' < m' using l' 1 2 3 LeastI[of ?P] by blast  

  have nretl': π' l'  return by (metis π''n πl' le_refl notπl)
 
  have nipd':  j  {k'..l'}. π' j  ipd (π' k') using lm' kk' ipd(2) kl' by force
 
  have lcd': l' cd⇗π'⇖→ k' by (metis is_cdi_def kl' nipd' nretl' path(2))

  have licd: l' icd⇗π'⇖→ k' proof -
    have  m  {k'<..<l'}. ¬ l' cd⇗π'⇖→ m proof (rule ccontr)
      assume ¬ ( m  {k'<..<l'}. ¬ l' cd⇗π'⇖→ m)
      then obtain j' where kj': k' < j' and jl': j' < l' and lcdj': l' cd⇗π'⇖→ j' by force
      have jm': j'<m' by (metis jl' lm' order.strict_trans)
      have π' j'  π l apply (rule ccontr) using l' kj' jm' jl' Least_le[of ?P j'] by auto       
      hence ¬ π' l' pd→ π' j' using cd_not_pd lcdj' πl' by metis
      moreover have π' j'  nodes using path(2) path_nodes by auto
      ultimately
      obtain π1 n1 where path1: is_path π1 and π01: π1 0 = π' j' and πn1: π1 n1 = return and nl':  l n1. π1 l  π' l' unfolding is_pd_def by blast
      let ?π'' = (π'@⇗j'π1) « Suc k'
      have is_path ?π'' by (metis π01 path(2) path1 path_cons path_path_shift)
      moreover
      have ?π'' 0 = π (Suc k) by (simp, metis kj' less_eq_Suc_le suc)
      moreover
      have kj': Suc k'  j' by (metis kj' less_eq_Suc_le)
      hence ?π'' (j' - Suc k' + n1) = return by (simp, metis π01 πn1)
      ultimately
      obtain l'' where *: ?π'' l'' = π l and **: l'' j' - Suc k' + n1 using lpd is_pd_def by blast      
      show False proof (cases)
        assume a: l''  j' - Suc k'        
        hence π' (l'' + Suc k') = π l using * kj' by(simp, metis Nat.le_diff_conv2 add_Suc diff_add_inverse le_add1 le_add_diff_inverse2)
        moreover 
        have l'' + Suc k' < l' by (metis a jl' add_diff_cancel_right' kj' le_add_diff_inverse less_imp_diff_less ordered_cancel_comm_monoid_diff_class.le_diff_conv2)
        moreover
        have l'' + Suc k' < m' by (metis Suc_lessD calculation(2) less_trans_Suc lm')
        moreover 
        have k' < l'' + Suc k' by simp
        ultimately
        show False using Least_le[of ?P l'' + Suc k'] l' by auto
      next
        assume a: ¬ l''  j' - Suc k'
        hence ¬ Suc (k' + l'')  j' by simp
        hence π1 (Suc (k' + l'') - j') = π l using * kj' by simp 
        moreover 
        have Suc (k' + l'') - j'  n1 using ** kj' by simp
        ultimately
        show False using nl' by (metis πl')
      qed
    qed
    thus ?thesis unfolding is_icdi_def using lcd' path(2) by simp
  qed
  hence ‹cs⇗π'l' = cs⇗π'k' @ [π' l'] by (metis icd_cs)
  hence ‹cs⇗π'l' = cs⇗πl by (metis πl' csk icd icd_cs)
  thus ?thesis by metis
qed

lemma converged_same_icd: assumes path: is_path π is_path π' and converge: l < n ‹cs⇗πn = cs⇗π'n' 
and csk: ‹cs⇗πk = cs⇗π'k' and icd: l icd⇗π⇖→ k and suc: π (Suc k) = π' (Suc k')
shows l'. cs⇗πl = cs⇗π'l' proof -
  
  have nret: π k  return using icd unfolding is_icdi_def is_cdi_def using term_path_stable less_imp_le by metis 
  have kl: k < l using icd unfolding is_icdi_def is_cdi_def by auto
  have kn: k < n using converge kl by simp
  from path_ipd_swap[OF path(1) nret kn]
  obtain ρ m where pathρ: is_path ρ and πρ: π =⇘nρ and km: k < m and ipd: ρ m = ipd (ρ k)  l  {k..<m}. ρ l  ipd (ρ k) .
  have csk1: ‹cs⇗ρk = cs⇗πk using cs_path_swap_le path pathρ πρ kn by auto
  have sucρ: ρ (Suc k) = π (Suc k) by (metis πρ eq_up_to_def kn less_eq_Suc_le)

  have nret': π' k'  return by (metis csk last_cs nret)
  have kn': k' < n' using cs_order[OF path csk converge(2) nret kn] .
  from path_ipd_swap[OF path(2) nret' kn']
  obtain ρ' m' where pathρ': is_path ρ' and πρ': π' =⇘n'ρ' and km': k' < m' and ipd': ρ' m' = ipd (ρ' k')  l  {k'..<m'}. ρ' l  ipd (ρ' k') .
  have csk1': ‹cs⇗ρ'k' = cs⇗π'k' using cs_path_swap_le path pathρ' πρ' kn' by auto
  have sucρ': ρ' (Suc k') = π' (Suc k') by (metis πρ' eq_up_to_def kn' less_eq_Suc_le)
  
  have icdρ: l icd⇗ρ⇖→ k using icdi_path_swap_le[OF pathρ icd πρ] converge by simp

  have lm: l < m using ipd(1) icdρ km unfolding is_icdi_def is_cdi_def by auto

  have csk': ‹cs⇗ρk = cs⇗ρ'k' using csk1 csk1' csk by auto

  hence kk': ρ' k' = ρ k using last_cs by metis

  have suc': ρ (Suc k) = ρ' (Suc k') using suc sucρ sucρ' by auto

  have mm': ρ' m' = ρ m using ipd(1) ipd'(1) kk' by auto

  from cs_ipd[OF ipd km] cs_ipd[OF ipd' km',unfolded mm', folded csk']  
  have csm: ‹cs⇗ρm = cs⇗ρ'm' by metis

  from converged_ipd_same_icd[OF pathρ pathρ' lm  csm csk' icdρ suc' ipd'[unfolded kk']]
  obtain l' where csl: ‹cs⇗ρl = cs⇗ρ'l' by blast
  
  have cslρ: ‹cs⇗πl = cs⇗ρl using πρ converge(1) cs_path_swap_le less_imp_le_nat path(1) pathρ by blast 

  have nretl: ρ l  return by (metis icdρ icd_imp_cd ret_no_cd)

  have csn': ‹cs⇗ρn = cs⇗ρ'n' using converge(2) cs_path_swap path pathρ pathρ' πρ πρ' by auto
  
  have ln': l' < n' using cs_order[OF pathρ pathρ' csl csn' nretl converge(1)] .
    
  have cslρ': ‹cs⇗π'l' = cs⇗ρ'l' using cs_path_swap_le[OF path(2) pathρ' πρ'] ln' by auto

  have csl': ‹cs⇗πl = cs⇗π'l' using cslρ cslρ' csl by auto
  thus ?thesis by blast
qed

lemma cd_is_cs_less: assumes l cd⇗π⇖→ k shows ‹cs⇗πk  cs⇗πl proof -
  obtain xs where csl: ‹cs⇗πl = cs⇗πk @ xs @[π l] using cd_in_cs[OF assms] by blast
  hence len: length(cs⇗πk) < length (cs⇗πl) by auto
  have take: take (length (cs⇗πk)) (cs⇗πl) = cs⇗πk using csl by auto
  show ?thesis using cs_less.intros[OF len take] . 
qed

lemma cs_select_id: assumes is_path π π k  return shows π¡cs⇗πk = k (is ?k = k) proof -
  have *:  i . cs⇗πi = cs⇗πk   i = k using cs_inj[OF assms] by metis  
  hence ‹cs⇗π?k = cs⇗πk unfolding cs_select_def using theI[of λ i. cs⇗πi = cs⇗πk k] by auto
  thus ?k = k using * by auto
qed

lemma cs_single_nocd: assumes ‹cs⇗πi = [x] shows  k. ¬ i cd⇗π⇖→ k proof -
  have ¬ ( k. i icd⇗π⇖→ k) apply (rule ccontr) using assms cs_not_nil by auto
  hence ¬ ( k. i cd⇗π⇖→ k) by (metis excd_impl_exicd)
  thus ?thesis by blast
qed

lemma cs_single_pd_intermed: assumes is_path π ‹cs⇗πn = [π n] k  n shows π n pd→ π k proof -
  have  l. ¬ n icd⇗π⇖→ l by (metis assms(2) cs_single_nocd icd_imp_cd)
  thus ?thesis by (metis assms(1) assms(3) no_icd_pd)
qed


lemma cs_first_pd:  assumes path: is_path π and pd: π n pd→ π 0 and first:  l < n. π l  π n shows ‹cs⇗πn = [π n] 
by (metis cs_cases first first_pd_no_cd icd_imp_cd path pd)

lemma converged_pd_cs_single: assumes path: is_path π is_path π' and  converge: l < m ‹cs⇗πm = cs⇗π'm' 
and π0: π 0 = π' 0 and mpdl: π m pd→ π l and csl: ‹cs⇗πl = [π l]
shows l'. cs⇗πl = cs⇗π'l' proof -
  have *: π l pd→ π' 0 using cs_single_pd_intermed[OF path(1) csl] π0[symmetric] by auto
  have πm: π m = π' m' by (metis converge(2) last_cs)
  hence **: π' m' pd→ π l using mpdl by metis
  
  obtain l' where lm': l'  m' and πl:  π' l' = π l (is ?P l') using path_pd_pd0[OF path(2) ** *] .
  
  let ?l = (LEAST l'. π' l' = π l)
  
  have πl': π' ?l = π l using LeastI[of ?P,OF πl] .
  moreover
  have  i <?l. π' i  π l using Least_le[of ?P] by (metis not_less)
  hence  i <?l. π' i  π' ?l using πl' by metis
  moreover
  have π' ?l pd→ π' 0 using * πl' by metis
  ultimately
  have ‹cs⇗π'?l = [π' ?l] using cs_first_pd[OF path(2)] by metis
  thus ?thesis using csl πl' by metis
qed

lemma converged_cs_single: assumes path: is_path π is_path π' and  converge: l < m ‹cs⇗πm = cs⇗π'm' 
and π0: π 0 = π' 0 and csl: ‹cs⇗πl = [π l]
shows l'. cs⇗πl = cs⇗π'l' proof cases
  assume *: π l = return  
  hence π m = return by (metis converge(1) path(1) term_path_stable less_imp_le)
  hence ‹cs⇗πm = [return] using cs_return by auto
  hence ‹cs⇗π'm' = [return] using converge by simp
  moreover
  have ‹cs⇗πl = [return] using * cs_return by auto
  ultimately show ?thesis by metis
next
  assume nret: π l  return
  have πm: π m = π' m' by (metis converge(2) last_cs)
  
  obtain π1 n where path1: is_path π1 and upto: π =⇘mπ1 and πn: π1 n = return using path(1) path_swap_ret by blast

  obtain π1' n' where path1': is_path π1' and upto': π' =⇘m'π1' and πn': π1' n' = return using path(2) path_swap_ret by blast

  have π1l: π1 l = π l using upto converge(1) by (metis eq_up_to_def nat_less_le)

  have cs1l: ‹cs⇗π1l = cs⇗πl using cs_path_swap_le upto path1 path(1) converge(1) by auto

  have csl1: ‹cs⇗π1l = [π1 l] by (metis π1l cs1l csl)
  
  have converge1: ‹cs⇗π1n = cs⇗π1'n' using πn πn' cs_return by auto
  
  have ln: l < n using nret πn π1l term_path_stable[OF path1 πn] by (auto, metis linorder_neqE_nat less_imp_le)

  have π01: π1 0 = π1' 0 using π0 eq_up_to_apply[OF upto] eq_up_to_apply[OF upto'] by auto

  have pd: π1 n pd→ π1 l using πn by (metis path1 path_nodes return_pd)
  
  obtain l' where csl: ‹cs⇗π1l = cs⇗π1'l' using converged_pd_cs_single[OF path1 path1' ln converge1 π01 pd csl1] by blast

  have cs1m: ‹cs⇗π1m = cs⇗πm using cs_path_swap upto path1 path(1) by auto
  have cs1m': ‹cs⇗π1'm' = cs⇗π'm' using cs_path_swap upto' path1' path(2) by auto
  hence converge1: ‹cs⇗π1m = cs⇗π1'm' using converge(2) cs1m by metis
  
  have nret1: π1 l  return using nret π1l by auto
  
  have lm': l' < m' using cs_order[OF path1 path1' csl converge1 nret1 converge(1)] .
  
  have ‹cs⇗π'l' = cs⇗π1'l' using cs_path_swap_le[OF path(2) path1' upto'] lm' by auto
  moreover
  have ‹cs⇗πl = cs⇗π1l using cs_path_swap_le[OF path(1) path1 upto] converge(1) by auto
  ultimately
  have ‹cs⇗πl = cs⇗π'l' using csl by auto
  thus ?thesis by blast
qed

lemma converged_cd_same_suc: assumes path: is_path π is_path π' and init: π 0 = π' 0 
and cd_suc:  k k'. cs⇗πk = cs⇗π'k'  l cd⇗π⇖→ k  π (Suc k) = π' (Suc k') and converge: l < m ‹cs⇗πm = cs⇗π'm' 
shows  l'. cs⇗πl = cs⇗π'l'
using path init cd_suc converge proof (induction π l rule: cs_induct,cases)
  case (cs π l)
  assume *: k. l icd⇗π⇖→ k
  let ?k = THE k. l icd⇗π⇖→ k
  have icd: l icd⇗π⇖→ ?k by (metis "*" icd_is_the_icd)
  hence lcdk: l cd⇗π⇖→ ?k by (metis is_icdi_def)
  hence kl: ?k<l using is_cdi_def by metis
  
  have  j. ?k cd⇗π⇖→ j  l cd⇗π⇖→ j using icd cd_trans is_icdi_def by fast
  hence suc':  j j'. cs⇗πj = cs⇗π'j'  ?k cd⇗π⇖→ j  π (Suc j) = π' (Suc j') using cs.prems(4) by blast

  from cs.IH[OF * cs(2) path(2) cs(4) suc'] cs.prems kl 
  have k'. cs⇗π(THE k. l icd⇗π⇖→ k) = cs⇗π'k' by (metis Suc_lessD less_trans_Suc)
  then obtain k' where csk: ‹cs⇗π?k = cs⇗π'k' by blast
  
  have suc2: π (Suc ?k) = π' (Suc k') using cs.prems(4) lcdk csk by auto

  have km: ?k < m using kl cs.prems(5) by simp
  
  from converged_same_icd[OF cs(2) path(2) cs.prems(5) cs.prems(6) csk icd suc2]  
  show ?case .
next
  case (cs π l)
  assume ¬ (k. l icd⇗π⇖→ k)
  hence ‹cs⇗πl = [π l] by auto
  with cs converged_cs_single
  show ?case by metis
qed

lemma converged_cd_diverge: 
assumes path: is_path π is_path π' and init: π 0 = π' 0 and notin: ¬ (l'. cs⇗πl = cs⇗π'l') and converge: l < m ‹cs⇗πm = cs⇗π'm' 
obtains k k' where ‹cs⇗πk = cs⇗π'k' l cd⇗π⇖→ k π (Suc k)  π' (Suc k')
using assms converged_cd_same_suc by blast



lemma converged_cd_same_suc_return: assumes path: is_path π is_path π' and π0: π 0 = π' 0 
and cd_suc:  k k'. cs⇗πk = cs⇗π'k'  l cd⇗π⇖→ k  π (Suc k) = π' (Suc k') and ret: π' n' = return 
shows  l'. cs⇗πl = cs⇗π'l'proof cases
  assume π l = return
  hence ‹cs⇗πl = cs⇗π'n' using ret cs_return by presburger
  thus ?thesis by blast
next
  assume nretl: π l  return
  have π l  nodes using path path_nodes by auto
  then obtain πl n where ipl: is_path πl and πl:  π l = πl 0 and retn: πl n = return and notl:  i>0. πl i  π l by (metis direct_path_return nretl)
  hence ip: is_path (π@⇗lπl) and l: (π@⇗lπl) l = π l and retl: (π@⇗lπl) (l + n) = return and nl:  i>l. (π@⇗lπl) i  π l using path_cons[OF path(1) ipl πl] by auto
  
  have π0': (π@⇗lπl) 0 = π' 0  unfolding cs_0 using  πl π0  by auto

  have csn: ‹cs⇗π@⇗lπl(l+n) = cs⇗π'n' using ret retl cs_return by metis

  have eql: (π@⇗lπl) =⇘lπ by (metis path_append_eq_up_to)    

  have csl': ‹cs⇗π@⇗lπll = cs⇗πl using eql cs_path_swap ip path(1) by metis
  
  have 0 < n using nretl[unfolded πl] retn by (metis neq0_conv)
  hence ln: l < l + n by simp

  have *:  k k'. cs⇗π @⇗lπlk = cs⇗π'k'  l cd⇗π @⇗lπl⇖→ k  (π @⇗lπl) (Suc k) = π' (Suc k') proof (rule,rule,rule)  
    fix k k' assume *: ‹cs⇗π @⇗lπlk = cs⇗π'k'  l cd⇗π @⇗lπl⇖→ k
    hence kl: k < l using is_cdi_def by auto
    hence ‹cs⇗πk = cs⇗π'k'  l cd⇗π⇖→ k using eql * cs_path_swap_le[OF ip path(1) eql,of k] cdi_path_swap_le[OF path(1) _ eql,of l k] by auto
    hence π (Suc k) = π' (Suc k') using cd_suc by blast
    then show (π @⇗lπl) (Suc k) = π' (Suc k') using cs_path_swap_le[OF ip path(1) eql,of Suc k] kl by auto
  qed 
  obtain l' where ‹cs⇗π @⇗lπll = cs⇗π'l' using converged_cd_same_suc[OF ip path(2) π0' * ln csn]  by blast
  moreover
  have ‹cs⇗π@⇗lπll = cs⇗πl using eql by (metis cs_path_swap ip path(1))
  ultimately
  show ?thesis by metis
qed

lemma converged_cd_diverge_return: assumes path: is_path π is_path π' and init: π 0 = π' 0 
and notin: ¬ (l'. cs⇗πl = cs⇗π'l') and ret: π' m' = return 
obtains k k' where ‹cs⇗πk = cs⇗π'k' l cd⇗π⇖→ k π (Suc k)  π' (Suc k') using converged_cd_same_suc_return[OF path init _ ret, of l] notin by blast

lemma returned_missing_cd_or_loop: assumes path: is_path π is_path π' and π0: π 0 = π' 0 
and notin': ¬( k'. cs⇗πk = cs⇗π'k') and nret:  n'. π' n'  return and ret: π n = return 
obtains i i' where i<k ‹cs⇗πi = cs⇗π'i' π (Suc i)  π' (Suc i') k cd⇗π⇖→ i  ( j'> i'. j' cd⇗π'⇖→ i')
proof -  
  obtain f where icdf:  i'. f (Suc i') icd⇗π'⇖→ f i' and ran: range f = {i'.  j'>i'. j' cd⇗π'⇖→ i'} and icdf0: ¬ (i'. f 0 cd⇗π'⇖→ i') using path(2) path_nret_inf_icd_seq nret by blast
  show thesis proof cases
    assume  j. ¬ ( i. cs⇗πi = cs⇗π'(f j))
    then obtain j where niπ: ¬ ( i. cs⇗π'(f j) = cs⇗πi) by metis
    note converged_cd_diverge_return[OF path(2,1) π0[symmetric] niπ ret] that
    then obtain i k' where csk: ‹cs⇗πi = cs⇗π'k' and cdj: f j cd⇗π'⇖→ k' and div:  π (Suc i)  π' (Suc k') by metis
    have k'  range f using cdj proof (induction j)
      case 0 thus ?case using icdf0 by blast
    next
      case (Suc j)
      have icdfj: f (Suc j) icd⇗π'⇖→ f j using icdf by auto
      show ?case proof cases
        assume f (Suc j) icd⇗π'⇖→ k'
        hence k' = f j using icdfj  by (metis icd_uniq)
        thus ?case by auto
      next
        assume ¬ f (Suc j) icd⇗π'⇖→ k'
        hence f j cd⇗π'⇖→ k' using cd_impl_icd_cd[OF Suc.prems icdfj] by auto
        thus ?case using Suc.IH by auto
      qed
    qed
    hence alldep:  i'>k'. i' cd⇗π'⇖→ k' using ran by auto
    show thesis proof cases
      assume i < k with alldep that[OF _ csk div] show thesis by blast
    next
      assume ¬ i < k
      hence ki: ki by auto
      have k  i using notin' csk by auto
      hence ki': k<i using ki by auto
      obtain ka k' where ‹cs⇗πka = cs⇗π'k' k cd⇗π⇖→ ka π (Suc ka)  π' (Suc k')
      using converged_cd_diverge[OF path π0 notin' ki' csk] by blast
      moreover
      hence ka < k unfolding is_cdi_def by auto
      ultimately
      show ?thesis using that by blast
    qed
  next
    assume ¬( j. ¬ ( i. cs⇗πi = cs⇗π'(f j)))
    hence allin:  j. ( i. cs⇗πi = cs⇗π'(f j)) by blast
    define f' where f': f'  λ j. (SOME i. cs⇗πi = cs⇗π'(f j))
    have  i. f' i < f' (Suc i) proof
      fix i
      have csi: ‹cs⇗π'(f i) = cs⇗π(f' i) unfolding f' using allin by (metis (mono_tags) someI_ex)
      have cssuci: ‹cs⇗π'(f (Suc i)) = cs⇗π(f' (Suc i)) unfolding f' using allin by (metis (mono_tags) someI_ex)
      have fi: f i < f (Suc i) using icdf unfolding is_icdi_def is_cdi_def by auto
      have f (Suc i) cd⇗π'⇖→ f i using icdf unfolding is_icdi_def by blast
      hence nreti: π' (f i)  return by (metis cd_not_ret)
      show f' i < f' (Suc i) using cs_order[OF path(2,1) csi cssuci nreti fi] .
    qed
    hence kle: k < f' (Suc k) using mono_ge_id[of f' Suc k] by auto
    have cssk: ‹cs⇗π(f' (Suc k)) = cs⇗π'(f (Suc k)) unfolding f' using allin by (metis (mono_tags) someI_ex)
    obtain ka k' where ‹cs⇗πka = cs⇗π'k' k cd⇗π⇖→ ka π (Suc ka)  π' (Suc k')
    using converged_cd_diverge[OF path π0 notin' kle cssk] by blast
    moreover
    hence ka < k unfolding is_cdi_def by auto
    ultimately
    show ?thesis using that by blast
  qed
qed

lemma missing_cd_or_loop: assumes path: is_path π is_path π' and π0: π 0 = π' 0 and notin': ¬( k'. cs⇗πk = cs⇗π'k')  
obtains i i' where i < k ‹cs⇗πi = cs⇗π'i' π (Suc i)  π' (Suc i') k cd⇗π⇖→ i  ( j'> i'. j' cd⇗π'⇖→ i')
proof cases
  assume  n'. π' n' = return
  then obtain n' where retn: π' n' = return by blast
  note converged_cd_diverge_return[OF path π0 notin' retn]
  then obtain ka k' where ‹cs⇗πka = cs⇗π'k' k cd⇗π⇖→ ka π (Suc ka)  π' (Suc k') by blast
  moreover
  hence ka < k unfolding is_cdi_def by auto
  ultimately show thesis using that by simp
next
  assume ¬ ( n'. π' n' = return)
  hence notret:  n'. π' n'  return by auto
  then obtain πl n where ipl: is_path πl and πl:  π k = πl 0 and retn: πl n = return using reaching_ret path(1) path_nodes by metis
  hence ip: is_path (π@⇗kπl) and l: (π@⇗kπl) k = π k and retl: (π@⇗kπl) (k + n) = return using path_cons[OF path(1) ipl πl] by auto
  
  have π0': (π@⇗kπl) 0 = π' 0  unfolding cs_0 using  πl π0  by auto

  have eql: (π@⇗kπl) =⇘kπ by (metis path_append_eq_up_to)    

  have csl': ‹cs⇗π@⇗kπlk = cs⇗πk using eql cs_path_swap ip path(1) by metis
  
  hence notin: ¬( k'. cs⇗π@⇗kπlk = cs⇗π'k') using notin' by auto

  obtain i i' where *: i < k and csi: ‹cs⇗π@⇗kπli = cs⇗π'i' and suci: (π @⇗kπl) (Suc i)  π' (Suc i')  and cdloop: k cd⇗π@⇗kπl⇖→ i  ( j'>i'. j' cd⇗π'⇖→ i')
  using returned_missing_cd_or_loop[OF ip path(2) π0' notin notret retl] by blast

  have i  k using notin csi by auto
  hence ik: i < k using * by auto
  hence ‹cs⇗πi = cs⇗π'i' using csi cs_path_swap_le[OF ip path(1) eql] by auto
  moreover
  have π (Suc i)  π' (Suc i') using ik eq_up_to_apply[OF eql, of Suc i] suci by auto
  moreover
  have k cd⇗π⇖→ i  ( j'>i'. j' cd⇗π'⇖→ i') using cdloop cdi_path_swap_le[OF path(1) _ eql, of k i] by auto
  ultimately
  show thesis using that[OF *] by blast
qed


lemma path_shift_set_cd: assumes is_path π shows {k + j| j . n cd⇗π«k⇖→ j } = {i. (k+n) cd⇗π⇖→ i  k  i }
proof -
  { fix i
    assume i{k+j | j . n cd⇗π«k⇖→ j }
    then obtain j where i = k+j n cd⇗π«k⇖→ j by auto
    hence k+n cd⇗π⇖→ i  k  i using cd_path_shift[OF _ assms, of k k+j k+n] by simp
    hence i{ i. k+n cd⇗π⇖→ i  k  i } by blast
  }
  moreover
  { fix i
    assume i{ i. k+n cd⇗π⇖→ i  k  i }
    hence *: k+n cd⇗π⇖→ i  k  i by blast
    then obtain j where i: i = k+j by (metis le_Suc_ex)
    hence k+n cd⇗π⇖→ k+j using * by auto
    hence n cd⇗π«k⇖→ j using cd_path_shift[OF _ assms, of k k+j k+n] by simp
    hence i{k+j | j . n cd⇗π«k⇖→ j } using i by simp
  }
  ultimately show ?thesis by blast
qed

lemma cs_path_shift_set_cd: assumes path: is_path π shows ‹cs⇗π«kn = map π (sorted_list_of_set {i. k+n cd⇗π⇖→ i  k  i }) @ [π (k+n)]
proof -
  have mono:n m. n < m  k + n < k + m by auto
  have fin: finite {i. n cd⇗π « k⇖→ i} unfolding is_cdi_def by auto
  have *: (λ x. k+x)`{i. n cd⇗π«k⇖→ i} = {k + i | i. n cd⇗π«k⇖→ i} by auto
  have ‹cs⇗π«kn = map (π«k) (sorted_list_of_set {i. n cd⇗π«k⇖→ i}) @ [(π«k) n] using cs_sorted_list_of_cd' by blast
  also 
  have  = map π (map (λ x. k+x) (sorted_list_of_set{i. n cd⇗π«k⇖→ i})) @ [π (k+n)] by auto
  also 
  have  = map π (sorted_list_of_set ((λ x. k+x)`{i. n cd⇗π«k⇖→ i})) @ [π (k+n)] using sorted_list_of_set_map_mono[OF mono fin] by auto
  also 
  have  = map π (sorted_list_of_set ({k + i | i. n cd⇗π«k⇖→ i})) @ [π (k+n)] using * by auto
  also 
  have  = map π (sorted_list_of_set ({i. k+n cd⇗π⇖→ i  k  i})) @ [π (k+n)] using path_shift_set_cd[OF path] by auto
  finally
  show ?thesis .
qed

lemma cs_split_shift_cd: assumes n cd⇗π⇖→ j and j < k and k < n and j'<k. n cd⇗π⇖→ j'  j'  j shows ‹cs⇗πn = cs⇗πj @ cs⇗π«k(n-k)
proof -
  have path: is_path π using assms unfolding is_cdi_def by auto
  have 1: {i. n cd⇗π⇖→ i} = {i. n cd⇗π⇖→ i  i < k}  {i. n cd⇗π⇖→ i  k  i} by auto
  have le:  i {i. n cd⇗π⇖→ i  i < k}.  j {i. n cd⇗π⇖→ i  k  i}. i < j by auto
  
  have 2: {i. n cd⇗π⇖→ i  i < k} = {i . j cd⇗π⇖→ i}  {j} proof - 
    { fix i assume i{i. n cd⇗π⇖→ i  i < k} 
      hence cd: n cd⇗π⇖→ i and ik:i < k by auto
      have i{i . j cd⇗π⇖→ i}  {j} proof cases
        assume i < j hence j cd⇗π⇖→ i by (metis is_cdi_def assms(1) cd cdi_prefix nat_less_le)
        thus ?thesis by simp
      next
        assume ¬ i < j
        moreover
        have i  j using assms(4) ik cd by auto
        ultimately
        show ?thesis by auto
      qed
    }
    moreover
    { fix i assume i{i . j cd⇗π⇖→ i}  {j}
      hence j cd⇗π⇖→ i  i = j by auto
      hence i{i. n cd⇗π⇖→ i  i < k} using assms(1,2) cd_trans[OF _ assms(1)] apply auto unfolding is_cdi_def 
      by (metis (poly_guards_query) diff_diff_cancel diff_is_0_eq le_refl le_trans nat_less_le)
    }
    ultimately show ?thesis by blast
  qed
  
  have ‹cs⇗πn = map π (sorted_list_of_set {i. n cd⇗π⇖→ i}) @ [π n] using cs_sorted_list_of_cd' by simp
  also 
  have  = map π (sorted_list_of_set ({i. n cd⇗π⇖→ i  i < k}  {i. n cd⇗π⇖→ i  k  i})) @ [π n] using 1 by metis
  also 
  have  = map π ((sorted_list_of_set {i. n cd⇗π⇖→ i  i < k}) @ (sorted_list_of_set {i. n cd⇗π⇖→ i  k  i})) @ [π n]
    using sorted_list_of_set_append[OF _ _ le] is_cdi_def by auto
  also 
  have  = (map π (sorted_list_of_set {i. n cd⇗π⇖→ i  i < k})) @ (map π (sorted_list_of_set {i. n cd⇗π⇖→ i  k  i})) @ [π n] by auto
  also
  have  = cs⇗πj @ (map π (sorted_list_of_set {i. n cd⇗π⇖→ i  k  i})) @ [π n] unfolding 2 using cs_sorted_list_of_cd by auto
  also 
  have  = cs⇗πj @ cs⇗π«k(n-k) using cs_path_shift_set_cd[OF path, of k n-k] assms(3) by auto
  finally
  show ?thesis .
qed

lemma cs_split_shift_nocd: assumes is_path π and k < n and j. n cd⇗π⇖→ j  k  j shows ‹cs⇗πn = cs⇗π«k(n-k)
proof -
  have path: is_path π using assms by auto
  have 1: {i. n cd⇗π⇖→ i} = {i. n cd⇗π⇖→ i  i < k}  {i. n cd⇗π⇖→ i  k  i} by auto
  have le:  i {i. n cd⇗π⇖→ i  i < k}.  j {i. n cd⇗π⇖→ i  k  i}. i < j by auto
  have 2: {i. n cd⇗π⇖→ i  i < k} = {} using assms by auto
  
  have ‹cs⇗πn = map π (sorted_list_of_set {i. n cd⇗π⇖→ i}) @ [π n] using cs_sorted_list_of_cd' by simp
  also 
  have  = map π (sorted_list_of_set ({i. n cd⇗π⇖→ i  i < k}  {i. n cd⇗π⇖→ i  k  i})) @ [π n] using 1 by metis
  also 
  have  = map π (sorted_list_of_set {i. n cd⇗π⇖→ i  k  i}) @ [π n]
    unfolding 2 by auto
  also 
  have  = cs⇗π«k(n-k) using cs_path_shift_set_cd[OF path, of k n-k] assms(2)  by auto
  finally show ?thesis .
qed

lemma shifted_cs_eq_is_eq: assumes is_path π and is_path π' and ‹cs⇗πk = cs⇗π'k' and ‹cs⇗π«kn = cs⇗π'«k'n' shows ‹cs⇗π(k+n) = cs⇗π'(k'+n')
proof (rule ccontr)
  note path = assms(1,2)
  note csk = assms(3)
  note csn = assms(4)
  assume ne: ‹cs⇗π(k+n)  cs⇗π'(k'+n')
  have nretkn:π (k+n)  return proof 
    assume 1:π (k+n) = return
    hence (π«k) n = return by auto
    hence (π'«k') n' = return using last_cs assms(4) by metis
    hence π' (k' + n') = return by auto
    thus False using ne 1 cs_return by auto
  qed
  hence nretk: π k  return using term_path_stable[OF assms(1), of k k +n] by auto
  have nretkn': π' (k'+n')  return proof 
    assume 1:π' (k'+n') = return
    hence (π'«k') n' = return by auto
    hence (π«k) n = return using last_cs assms(4) by metis
    hence π (k + n) = return by auto
    thus False using ne 1 cs_return by auto
  qed
  hence nretk': π' k'  return using term_path_stable[OF assms(2), of k' k' +n'] by auto
  have n0:n > 0 proof (rule ccontr)
    assume *: ¬ 0 < n    
    hence 1:‹cs⇗π«k0 = cs⇗π'«k'n' using assms(3,4) by auto
    have (π«k) 0 = (π'«k') 0 using assms(3) last_cs path_shift_def by (metis monoid_add_class.add.right_neutral)
    hence ‹cs⇗π'«k'0 = cs⇗π'«k'n' using 1 cs_0 by metis
    hence n0': n' = 0 using cs_inj[of π'«k' 0 n' ] * assms(2) by (metis path_shift_def assms(4) last_cs nretkn path_path_shift)
    thus False using ne * assms(3) by fastforce
  qed
  have n0':n' > 0 proof (rule ccontr)
    assume *: ¬ 0 < n'    
    hence 1:‹cs⇗π'«k'0 = cs⇗π«kn using assms(3,4) by auto
    have (π'«k') 0 = (π«k) 0 using assms(3) last_cs path_shift_def by (metis monoid_add_class.add.right_neutral)
    hence ‹cs⇗π«k0 = cs⇗π«kn using 1 cs_0 by metis
    hence n0: n = 0 using cs_inj[of π«k 0 n ] * assms(1) by (metis path_shift_def assms(4) last_cs nretkn path_path_shift)
    thus False using ne * assms(3) by fastforce
  qed
  have cdleswap':  j'<k'. (k'+n') cd⇗π'⇖→ j'  (j<k. (k+n) cd⇗π⇖→ j  cs⇗πj = cs⇗π'j') proof (rule,rule,rule, rule ccontr)
    fix j' assume jk': j'<k' and ncdj': (k'+n') cd⇗π'⇖→ j' and ne: ¬ (j<k. k + n cd⇗π⇖→ j  cs⇗πj = cs⇗π'j')
    hence kcdj': k' cd⇗π'⇖→ j' using cr_wn' by blast 
      
      then obtain j where kcdj: k cd⇗π⇖→ j and csj: ‹cs⇗πj = cs⇗π'j' using csk cs_path_swap_cd path by metis
      hence jk: j < k unfolding is_cdi_def by auto
      
      have ncdn: ¬ (k+n) cd⇗π⇖→ j using ne csj jk by blast 
      
      obtain l' where lnocd': l' = n'  n' cd⇗π'«k'⇖→ l' and cslsing': ‹cs⇗π'«k'l' = [(π'«k') l']        
        proof cases
          assume ‹cs⇗π'«k'n' = [(π'«k') n'] thus thesis using that[of n'] by auto
        next
          assume *: ‹cs⇗π'«k'n'  [(π'«k') n']
          then obtain x ys where ‹cs⇗π'«k'n' = [x]@ys@[(π'«k') n'] by (metis append_Cons append_Nil cs_length_g_one cs_length_one(1) neq_Nil_conv) 
          then obtain l' where ‹cs⇗π'«k'l' = [x] and cdl': n' cd⇗π'«k'⇖→ l' using cs_split[of π'«k' n' Nil x ys] by auto
          hence ‹cs⇗π'«k'l' = [(π'«k') l'] using last_cs by (metis last.simps) 
          thus thesis using that cdl' by auto
      qed
      hence ln': l'n' unfolding is_cdi_def by auto
      hence lcdj': k'+l' cd⇗π'⇖→ j' using jk' ncdj'  by (metis add_le_cancel_left cdi_prefix trans_less_add1)
            
      obtain l where lnocd: l = n  n cd⇗π«k⇖→ l and csl: ‹cs⇗π«kl = cs⇗π'«k'l' using lnocd' proof
        assume l' = n' thus thesis using csn that[of n] by auto
        next
        assume n' cd⇗π'«k'⇖→ l'
        then obtain l where n cd⇗π«k⇖→ l ‹cs⇗π«kl = cs⇗π'«k'l' using cs_path_swap_cd path csn by (metis path_path_shift)
        thus thesis using that by auto
      qed
      
      have cslsing: ‹cs⇗π«kl = [(π«k) l] using cslsing' last_cs csl last.simps by metis
      
      have ln: ln using lnocd unfolding is_cdi_def by auto
      hence nretkl: π (k + l)  return using term_path_stable[of π k+l k+n] nretkn path(1) by auto  
      
      have *: n cd⇗π«k⇖→ l  k+n cd⇗π⇖→ k+l using cd_path_shift[of k k+l π k+n] path(1) by auto
      
      have ncdl: ¬ (k+l) cd⇗π⇖→ j apply rule using lnocd apply rule using ncdn apply blast using cd_trans ncdn * by blast      
      
      hence  i {j..k+l}. π i = ipd (π j) unfolding is_cdi_def using path(1) jk nretkl by auto
      hence  i {k<..k+l}. π i = ipd (π j) using kcdj unfolding is_cdi_def by force
      
      then obtain i where ki: k < i and il: i  k+l and ipdi: π i = ipd (π j) by force
      
      hence (π«k) (i-k) = ipd (π j) i-k  l by auto
      hence pd: (π«k) l pd→ ipd (π j) using cs_single_pd_intermed[OF _ cslsing] path(1) path_path_shift by metis
      moreover
      have (π«k) l = π' (k' + l') using csl last_cs by (metis path_shift_def)
      moreover
      have π j = π' j' using csj last_cs by metis
      ultimately
      have π' (k'+l') pd→ ipd (π' j') by simp
      moreover
      have ipd (π' j') pd→ π' (k'+l') using ipd_pd_cd[OF lcdj'] .
      ultimately
      have π' (k'+l') = ipd (π' j') using pd_antisym by auto
      thus False using lcdj' unfolding is_cdi_def by force
  qed
  
  ― ‹Symmetric version of the above statement›
  have cdleswap:  j<k. (k+n) cd⇗π⇖→ j  (j'<k'. (k'+n') cd⇗π'⇖→ j'  cs⇗πj = cs⇗π'j') proof (rule,rule,rule, rule ccontr)
    fix j assume jk: j<k and ncdj: (k+n) cd⇗π⇖→ j and ne: ¬ (j'<k'. k' + n' cd⇗π'⇖→ j'  cs⇗πj = cs⇗π'j')
    hence kcdj: k cd⇗π⇖→ j using cr_wn' by blast
      
      then obtain j' where kcdj': k' cd⇗π'⇖→ j' and csj: ‹cs⇗πj = cs⇗π'j' using csk cs_path_swap_cd path by metis
      hence jk': j' < k' unfolding is_cdi_def by auto
      
      have ncdn': ¬ (k'+n') cd⇗π'⇖→ j' using ne csj jk' by blast 
      
      obtain l where lnocd: l = n  n cd⇗π«k⇖→ l and cslsing: ‹cs⇗π«kl = [(π«k) l]        
        proof cases
          assume ‹cs⇗π«kn = [(π«k) n] thus thesis using that[of n] by auto
        next
          assume *: ‹cs⇗π«kn  [(π«k) n]
          then obtain x ys where ‹cs⇗π«kn = [x]@ys@[(π«k) n] by (metis append_Cons append_Nil cs_length_g_one cs_length_one(1) neq_Nil_conv) 
          then obtain l where ‹cs⇗π«kl = [x] and cdl: n cd⇗π«k⇖→ l using cs_split[of π«k n Nil x ys] by auto
          hence ‹cs⇗π«kl = [(π«k) l] using last_cs by (metis last.simps) 
          thus thesis using that cdl by auto
      qed
      hence ln: ln unfolding is_cdi_def by auto
      hence lcdj: k+l cd⇗π⇖→ j using jk ncdj  by (metis add_le_cancel_left cdi_prefix trans_less_add1)
            
      obtain l' where lnocd': l' = n'  n' cd⇗π'«k'⇖→ l' and csl: ‹cs⇗π«kl = cs⇗π'«k'l' using lnocd proof
        assume l = n thus thesis using csn that[of n'] by auto
        next
        assume n cd⇗π«k⇖→ l
        then obtain l' where n' cd⇗π'«k'⇖→ l' ‹cs⇗π«kl = cs⇗π'«k'l' using cs_path_swap_cd path csn by (metis path_path_shift)
        thus thesis using that by auto
      qed
      
      have cslsing': ‹cs⇗π'«k'l' = [(π'«k') l'] using cslsing last_cs csl last.simps by metis
      
      have ln': l'n' using lnocd' unfolding is_cdi_def by auto
      hence nretkl': π' (k' + l')  return using term_path_stable[of π' k'+l' k'+n'] nretkn' path(2) by auto  
      
      have *: n' cd⇗π'«k'⇖→ l'  k'+n' cd⇗π'⇖→ k'+l' using cd_path_shift[of k' k'+l' π' k'+n'] path(2) by auto
      
      have ncdl': ¬ (k'+l') cd⇗π'⇖→ j' apply rule using lnocd' apply rule using ncdn' apply blast using cd_trans ncdn' * by blast      
      
      hence  i' {j'..k'+l'}. π' i' = ipd (π' j') unfolding is_cdi_def using path(2) jk' nretkl' by auto
      hence  i' {k'<..k'+l'}. π' i' = ipd (π' j') using kcdj' unfolding is_cdi_def by force
      
      then obtain i' where ki': k' < i' and il': i'  k'+l' and ipdi: π' i' = ipd (π' j') by force
      
      hence (π'«k') (i'-k') = ipd (π' j') i'-k'  l' by auto
      hence pd: (π'«k') l' pd→ ipd (π' j') using cs_single_pd_intermed[OF _ cslsing'] path(2) path_path_shift by metis
      moreover
      have (π'«k') l' = π (k + l) using csl last_cs by (metis path_shift_def)
      moreover
      have π' j' = π j using csj last_cs by metis
      ultimately
      have π (k+l) pd→ ipd (π j) by simp
      moreover
      have ipd (π j) pd→ π (k+l) using ipd_pd_cd[OF lcdj] .
      ultimately
      have π (k+l) = ipd (π j) using pd_antisym by auto
      thus False using lcdj unfolding is_cdi_def by force
  qed
  
  have cdle: j. (k+n) cd⇗π⇖→ j  j < k (is  j. ?P j) proof (rule ccontr)
    assume ¬ (j. (k+n) cd⇗π⇖→ j  j < k)
    hence allge: j. (k+n) cd⇗π⇖→ j  k  j by auto
    have allge': j'. (k'+n') cd⇗π'⇖→ j'  k'  j' proof (rule, rule, rule ccontr)
      fix j' 
      assume *: k' + n' cd⇗π'⇖→ j' and ¬ k'  j'
      then obtain j where j<k (k+n) cd⇗π⇖→ j using cdleswap' by (metis le_neq_implies_less nat_le_linear)
      thus False using allge by auto
    qed
    have ‹cs⇗π(k + n) = cs⇗π « kn using cs_split_shift_nocd[OF assms(1) _ allge] n0 by auto
    moreover
    have ‹cs⇗π'(k' + n') = cs⇗π' « k'n' using cs_split_shift_nocd[OF assms(2) _ allge'] n0' by auto
    ultimately
    show False using ne assms(4) by auto
  qed
  
  define j where  j == GREATEST j. (k+n) cd⇗π⇖→ j  j < k  
  have cdj:(k+n) cd⇗π⇖→ j and jk: j < k and jge: j'< k. (k+n) cd⇗π⇖→ j'  j'  j proof -
    have bound:  y. ?P y  y  k by auto
    show (k+n) cd⇗π⇖→ j using GreatestI_nat[of ?P] j_def bound cdle by blast
    show j < k using GreatestI_nat[of ?P] bound j_def cdle by blast
    show  j'< k. (k+n) cd⇗π⇖→ j'  j'  j using Greatest_le_nat[of ?P] bound j_def by blast
  qed
    
  obtain j' where cdj':(k'+n') cd⇗π'⇖→ j' and csj: ‹cs⇗πj = cs⇗π'j'  and jk': j' < k' using cdleswap cdj jk by blast
  have jge': i'< k'. (k'+n') cd⇗π'⇖→ i'  i'  j' proof(rule,rule,rule)
    fix i'
    assume ik': i' < k' and cdi': k' + n' cd⇗π'⇖→ i'
    then obtain i where cdi:(k+n) cd⇗π⇖→ i and csi: ‹ cs⇗π'i' = cs⇗πi and ik: i<k using cdleswap' by force 
    have ij: i  j using jge cdi ik by auto
    show i'  j' using cs_order_le[OF assms(1,2) csi[symmetric] csj _ ij] cd_not_ret[OF cdi] by simp
  qed
  have ‹cs⇗π(k + n) = cs⇗πj @ cs⇗π « kn using  cs_split_shift_cd[OF cdj jk _ jge] n0 by auto
  moreover
  have ‹cs⇗π'(k' + n') = cs⇗π'j' @ cs⇗π' « k'n' using  cs_split_shift_cd[OF cdj' jk' _ jge'] n0' by auto
  ultimately
  have ‹cs⇗π(k+n) = cs⇗π'(k'+n') using csj assms(4) by auto
  thus False using ne by simp
qed

lemma cs_eq_is_eq_shifted: assumes is_path π and is_path π' and ‹cs⇗πk = cs⇗π'k' and ‹cs⇗π(k+n) = cs⇗π'(k'+n') shows ‹cs⇗π«kn = cs⇗π'«k'n'
proof (rule ccontr)
  assume ne: ‹cs⇗π « kn  cs⇗π' « k'n'
  have nretkn:π (k+n)  return proof 
    assume 1:π (k+n) = return
    hence 2:π' (k'+n') = return using assms(4) last_cs by metis
    hence (π«k) n = return (π'«k') n' = return using 1 by auto
    hence ‹cs⇗π « kn = cs⇗π' « k'n' using cs_return by metis 
    thus False using ne by simp
  qed
  hence nretk: π k  return using term_path_stable[OF assms(1), of k k +n] by auto
  have nretkn': π' (k'+n')  return proof 
    assume 1:π' (k'+n') = return
    hence 2:π (k+n) = return using assms(4) last_cs by metis
    hence (π«k) n = return (π'«k') n' = return using 1 by auto
    hence ‹cs⇗π « kn = cs⇗π' « k'n' using cs_return by metis 
    thus False using ne by simp
  qed
  hence nretk': π' k'  return using term_path_stable[OF assms(2), of k' k' +n'] by auto
  have n0:n > 0 proof (rule ccontr)
    assume *: ¬ 0 < n    
    hence ‹cs⇗π'k' = cs⇗π'(k'+ n') using assms(3,4) by auto
    hence n0: n = 0 n' = 0 using cs_inj[OF assms(2) nretkn', of k'] * by auto
    have ‹cs⇗π « kn = cs⇗π' « k'n' unfolding n0 cs_0 by (auto , metis last_cs assms(3))
    thus False using ne by simp
  qed
  have n0':n' > 0 proof (rule ccontr)
    assume *: ¬ 0 < n'    
    hence ‹cs⇗πk = cs⇗π(k+ n) using assms(3,4) by auto
    hence n0: n = 0 n' = 0 using cs_inj[OF assms(1) nretkn, of k] * by auto
    have ‹cs⇗π « kn = cs⇗π' « k'n' unfolding n0 cs_0 by (auto , metis last_cs assms(3))
    thus False using ne by simp
  qed
  have cdle: j. (k+n) cd⇗π⇖→ j  j < k (is  j. ?P j) proof (rule ccontr)
    assume ¬ (j. (k+n) cd⇗π⇖→ j  j < k)
    hence allge: j. (k+n) cd⇗π⇖→ j  k  j by auto
    have allge': j'. (k'+n') cd⇗π'⇖→ j'  k'  j' proof (rule, rule)
      fix j' 
      assume *: k' + n' cd⇗π'⇖→ j'
      obtain j where cdj: k+n cd⇗π⇖→ j and csj: ‹cs⇗πj = cs⇗π'j' using cs_path_swap_cd[OF assms(2,1) assms(4)[symmetric] *] by metis
      hence kj:k  j using allge by auto
      thus kj': k'  j' using cs_order_le[OF assms(1,2,3) csj nretk] by simp
    qed
    have ‹cs⇗π(k + n) = cs⇗π « kn using cs_split_shift_nocd[OF assms(1) _ allge] n0 by auto
    moreover
    have ‹cs⇗π'(k' + n') = cs⇗π' « k'n' using cs_split_shift_nocd[OF assms(2) _ allge'] n0' by auto
    ultimately
    show False using ne assms(4) by auto
  qed
  define j where  j == GREATEST j. (k+n) cd⇗π⇖→ j  j < k  
  have cdj:(k+n) cd⇗π⇖→ j and jk: j < k and jge: j'< k. (k+n) cd⇗π⇖→ j'  j'  j proof -
    have bound:  y. ?P y  y  k by auto
    show (k+n) cd⇗π⇖→ j using GreatestI_nat[of ?P] bound j_def cdle by blast
    show j < k using GreatestI_nat[of ?P] bound j_def cdle by blast
    show  j'< k. (k+n) cd⇗π⇖→ j'  j'  j using Greatest_le_nat[of ?P] bound j_def by blast
  qed
  obtain j' where cdj':(k'+n') cd⇗π'⇖→ j' and csj: ‹cs⇗πj = cs⇗π'j' using cs_path_swap_cd assms cdj by blast
  have jge': i'< k'. (k'+n') cd⇗π'⇖→ i'  i'  j' proof(rule,rule,rule)
    fix i'
    assume ik': i' < k' and cdi': k' + n' cd⇗π'⇖→ i'
    then obtain i where cdi:(k+n) cd⇗π⇖→ i and csi: ‹ cs⇗π'i' = cs⇗πi using cs_path_swap_cd[OF assms(2,1) assms(4)[symmetric]] by blast
    have nreti': π' i'  return by (metis cd_not_ret cdi')
    have ik: i < k using cs_order[OF assms(2,1) csi _ nreti' ik'] assms(3) by auto
    have ij: i  j using jge cdi ik by auto
    show i'  j' using cs_order_le[OF assms(1,2) csi[symmetric] csj _ ij] cd_not_ret[OF cdi] by simp
  qed
  have jk': j' < k' using cs_order[OF assms(1,2) csj assms(3) cd_not_ret[OF cdj] jk] .
  have ‹cs⇗π(k + n) = cs⇗πj @ cs⇗π « kn using  cs_split_shift_cd[OF cdj jk _ jge] n0 by auto
  moreover
  have ‹cs⇗π'(k' + n') = cs⇗π'j' @ cs⇗π' « k'n' using  cs_split_shift_cd[OF cdj' jk' _ jge'] n0' by auto
  ultimately
  have ‹cs⇗π«kn = cs⇗π'«k'n' using csj assms(4) by auto
  thus False using ne by simp
qed

lemma converged_cd_diverge_cs: assumes is_path π and is_path π' and ‹cs⇗πj  = cs⇗π'j' and j<l and ¬ (l'. cs⇗πl = cs⇗π'l') and l < m and ‹cs⇗πm = cs⇗π'm'
obtains k k' where jk ‹cs⇗πk = cs⇗π'k' and l cd⇗π⇖→ k and π (Suc k)  π' (Suc k')
  proof -  
  have is_path (π«j) is_path (π'«j') using assms(1,2) path_path_shift by auto
  moreover
  have (π«j) 0 = (π'«j') 0 using assms(3) last_cs by (metis path_shift_def add.right_neutral)
  moreover
  have ¬(l'. cs⇗π«j(l-j) = cs⇗π'«j'l') proof 
    assume l'. cs⇗π « j(l - j) = cs⇗π' « j'l'
    then obtain l' where csl: ‹cs⇗π«j(l - j) = cs⇗π'«j'l' by blast
      
    have ‹cs⇗πl = cs⇗π'(j' + l') using shifted_cs_eq_is_eq[OF assms(1,2,3) csl] assms(4) by auto
    thus False using assms(5) by blast
  qed
  moreover
  have l-j < m-j using assms by auto
  moreover
  have π j  return using cs_return assms(1-5) term_path_stable by (metis nat_less_le) 
  hence j'<m' using cs_order[OF assms(1,2,3,7)] assms by auto
  hence ‹cs⇗π«j(m-j) = cs⇗π'«j'(m'-j') using cs_eq_is_eq_shifted[OF assms(1,2,3),of m-j m'-j'] assms(4,6,7) by auto
  ultimately
  obtain k k' where csk: ‹cs⇗π«jk = cs⇗π'«j'k' and lcdk: l-j cd⇗π«j⇖→ k and suc:(π«j) (Suc k)  (π'«j') (Suc k') using converged_cd_diverge by blast
  
  have ‹cs⇗π(j+k) = cs⇗π'(j'+k') using shifted_cs_eq_is_eq[OF assms(1-3) csk] .
  moreover
  have l cd⇗π⇖→ j+k using lcdk assms(1,2,4) by (metis add.commute add_diff_cancel_right' cd_path_shift le_add1)
  moreover
  have π (Suc (j+k))  π' (Suc (j'+ k')) using suc by auto
  moreover
  have j  j+k by auto
  ultimately
  show thesis using that[of j+k j'+k'] by auto
qed


lemma cs_ipd_conv: assumes csk: ‹cs⇗πk = cs⇗π'k' and ipd: π l = ipd (π k) π' l' = ipd(π' k') 
  and nipd: n{k..<l}. π n  ipd (π k) n'{k'..<l'}. π' n'  ipd (π' k') and kl: k < l k' < l' 
shows ‹cs⇗πl = cs⇗π'l' using cs_ipd[OF ipd(1) nipd(1) kl(1)] cs_ipd[OF ipd(2) nipd(2) kl(2)] csk ipd by (metis (no_types) last_cs)

lemma cp_eq_cs: assumes ((σ,k),(σ',k'))cp shows ‹cs⇗path σk = cs⇗path σ'k' 
  using assms 
  apply(induction rule: cp.induct) 
     apply blast+ 
  apply simp 
  done 

lemma cd_cs_swap: assumes l cd⇗π⇖→ k ‹cs⇗πl = cs⇗π'l' ‹cs⇗πk = cs⇗π'k' shows l' cd⇗π'⇖→ k' proof -
  have  i. l icd⇗π⇖→ i using assms(1) excd_impl_exicd by blast
  hence ‹cs⇗πl  [π l] by auto
  hence ‹cs⇗π'l'  [π' l'] using assms last_cs by metis
  hence  i'. l' icd⇗π'⇖→ i' by (metis cs_cases)
  hence path': is_path π' unfolding is_icdi_def is_cdi_def by auto
  from cd_in_cs[OF assms(1)]
  obtain ys where csl: ‹cs⇗πl = cs⇗πk @ ys @ [π l] by blast
  obtain xs where csk: ‹cs⇗πk = xs@[π k] by (metis append_butlast_last_id cs_not_nil last_cs)
  have πl: π l = π' l' using assms last_cs by metis
  have csl': ‹cs⇗π'l' = xs@[π k]@ys@[π' l'] by (metis πl append_eq_appendI assms(2) csk csl)
  from cs_split[of π' l' xs π k ys]
  obtain m where csm: ‹cs⇗π'm = xs @ [π k] and lcdm: l' cd⇗π'⇖→ m using csl' by metis 
  have csm': ‹cs⇗π'm = cs⇗π'k' by (metis assms(3) csk csm)
  have π' m  return using lcdm unfolding is_cdi_def using term_path_stable by (metis nat_less_le)
  hence m = k' using cs_inj path' csm' by auto
  thus ?thesis using lcdm by auto
qed


subsection ‹Facts about Observations›
lemma kth_obs_not_none: assumes is_kth_obs (path σ) k i obtains a where obsp σ i = Some a using assms unfolding is_kth_obs_def obsp_def by auto

lemma kth_obs_unique: is_kth_obs π k i  is_kth_obs π k j  i = j proof (induction i j rule: nat_sym_cases)
  case sym thus ?case by simp
next
  case eq thus ?case by simp
next
  case (less i j) 
  have obs_ids π  {..<i}  obs_ids π  {..<j} using less(1) by auto
  moreover
  have i  obs_ids π  {..<j} using less unfolding is_kth_obs_def obs_ids_def by auto
  moreover  
  have i  obs_ids π  {..<i} by auto
  moreover 
  have card (obs_ids π  {..<i}) = card (obs_ids π  {..<j}) using less.prems unfolding is_kth_obs_def by auto
  moreover
  have finite (obs_ids π  {..<i}) finite (obs_ids π  {..<j}) by auto
  ultimately 
  have False by (metis card_subset_eq)
  thus ?case ..
qed

lemma obs_none_no_kth_obs: assumes obs σ k = None shows ¬ ( i. is_kth_obs (path σ) k i) 
  apply rule
  using assms 
  unfolding obs_def obsp_def 
  apply (auto split: option.split_asm)  
  by (metis assms kth_obs_not_none kth_obs_unique obs_def option.distinct(2) the_equality)

lemma obs_some_kth_obs : assumes obs σ k  None obtains i where is_kth_obs (path σ) k i by (metis obs_def assms)

lemma not_none_is_obs: assumes att(π i)  None shows is_kth_obs π (card (obs_ids π  {..<i})) i  unfolding is_kth_obs_def using assms by auto

lemma in_obs_ids_is_kth_obs: assumes i  obs_ids π obtains k where is_kth_obs π k i proof 
  have att (π i)  None using assms obs_ids_def by auto 
  thus is_kth_obs π (card (obs_ids π  {..<i})) i using not_none_is_obs by auto
qed

lemma kth_obs_stable: assumes is_kth_obs π l j k < l shows  i. is_kth_obs π k i using assms proof (induction l arbitrary: j rule: less_induct )
  case (less l j)
  have cardl: card (obs_ids π  {..<j}) = l using less is_kth_obs_def by auto
  then obtain i where  ex: i  obs_ids π  {..<j} (is ?P i) using less(3) by (metis card.empty empty_iff less_irrefl subsetI subset_antisym zero_diff zero_less_diff)
  have bound:  i. i  obs_ids π  {..<j}  i  j by auto
  let ?i = GREATEST i. i  obs_ids π  {..<j}
  have *: ?i < j ?i  obs_ids π using GreatestI_nat[of ?P i j] ex bound by auto
  have **:  i. i  obs_ids π  i<j  i  ?i using Greatest_le_nat[of ?P _ j] ex bound by auto
  have (obs_ids π  {..<?i})  {?i} = obs_ids π  {..<j} apply rule apply auto using *[simplified] apply simp+ using **[simplified] by auto
  moreover
  have ?i  (obs_ids π  {..<?i}) by auto
  ultimately
  have Suc (card (obs_ids π  {..<?i})) = l using cardl by (metis Un_empty_right Un_insert_right card_insert_disjoint finite_Int finite_lessThan)
  hence card (obs_ids π  {..<?i}) = l - 1 by auto
  hence iko: is_kth_obs π (l - 1) ?i using *(2) unfolding is_kth_obs_def obs_ids_def by auto
  have ll: l - 1 < l by (metis One_nat_def diff_Suc_less less.prems(2) not_gr0 not_less0)
  note IV=less(1)[OF ll iko]
  show ?thesis proof cases
    assume k < l - 1 thus ?thesis using IV by simp
  next
    assume ¬ k < l - 1
    hence k = l - 1 using less by auto
    thus ?thesis using iko by blast
  qed
qed

lemma kth_obs_mono: assumes is_kth_obs π k i is_kth_obs π l j k < l shows i < j proof (rule ccontr)
  assume ¬ i < j
  hence {..<j}  {..<i} by auto
  hence obs_ids π  {..<j}  obs_ids π  {..<i} by auto
  moreover 
  have finite (obs_ids π  {..<i}) by auto
  ultimately
  have card (obs_ids π  {..<j})  card (obs_ids π  {..<i}) by (metis card_mono)
  thus False using assms unfolding is_kth_obs_def by auto
qed

lemma kth_obs_le_iff: assumes is_kth_obs π k i is_kth_obs π l j  shows k < l  i < j by (metis assms kth_obs_unique kth_obs_mono not_less_iff_gr_or_eq)

lemma ret_obs_all_obs: assumes path: is_path π and iki: is_kth_obs π k i and ret: π i = return and kl: k < l obtains j where is_kth_obs π l j
proof-
  show thesis
  using kl iki ret proof (induction l - k arbitrary: k i rule: less_induct)
    case (less k i)
    note kl = k < l
    note iki = is_kth_obs π k i
    note ret = π i = return  
    have card: card (obs_ids π  {..<i}) = k and att_ret: att return  Noneusing iki ret unfolding is_kth_obs_def by auto
    have rets: π (Suc i) = return using path ret term_path_stable by auto
    hence attsuc: att (π (Suc i))  None using att_ret by auto
    hence *: i  obs_ids π using att_ret ret unfolding obs_ids_def by auto
    have {..< Suc i} = insert i {..<i} by auto
    hence a: obs_ids π  {..< Suc i} = insert i (obs_ids π  {..<i}) using * by auto
    have b: i  obs_ids π  {..<i} by auto
    have finite (obs_ids π  {..<i}) by auto
    hence card (obs_ids π  {..<Suc i}) = Suc k by (metis card card_insert_disjoint a b)
    hence iksuc: is_kth_obs π (Suc k) (Suc i) using attsuc unfolding is_kth_obs_def by auto
    have suckl: Suc k  l using kl by auto
    note less
    thus thesis proof (cases Suc k < l) 
      assume skl: Suc k < l 
      from less(1)[OF _ skl iksuc rets] skl
      show thesis by auto
    next
      assume ¬ Suc k < l
      hence Suc k = l using suckl by auto
      thus thesis using iksuc that by auto
    qed
  qed
qed

lemma no_kth_obs_missing_cs: assumes path: is_path π is_path π' and iki: is_kth_obs π k i and not_in_π': ¬(i'. is_kth_obs π' k i')  obtains  l j where is_kth_obs π l j ¬ ( j'. cs⇗πj = cs⇗π'j')
proof (rule ccontr)
  assume ¬ thesis
  hence all_in_π':  l j. is_kth_obs π l j  ( j' . cs⇗πj = cs⇗π'j') using that by blast
  then obtain i' where csi: ‹cs⇗πi = cs⇗π'i' using assms by blast    
  hence att(π' i')  None using iki by (metis is_kth_obs_def last_cs)
  then obtain k' where ik': is_kth_obs π' k' i' by (metis not_none_is_obs)
  hence kk': k' < k using not_in_π' kth_obs_stable by (auto, metis not_less_iff_gr_or_eq)
  show False proof (cases π i = return)
    assume π i  return
    thus False using kk' ik' csi iki proof (induction k arbitrary: i i' k' )
      case 0 thus ?case by simp
    next
      case (Suc k i i' k')      
      then obtain j where ikj: is_kth_obs π k j by (metis kth_obs_stable lessI)
      then obtain j' where csj: ‹cs⇗πj = cs⇗π'j' using all_in_π' by blast    
      hence att(π' j')  None using ikj by (metis is_kth_obs_def last_cs)
      then obtain k2 where ik2: is_kth_obs π' k2 j' by (metis not_none_is_obs)
      have ji: j < i using kth_obs_mono [OF ikj is_kth_obs π (Suc k) i] by auto
      hence nretj: π j  return using Suc(2) term_path_stable less_imp_le path(1) by metis    
      have ji': j' < i' using cs_order[OF path _ _ nretj, of j' i i'] csj ‹cs⇗πi = cs⇗π'i'  ji by auto
      have k2  k' using ik2 Suc(4) ji' kth_obs_unique[of π' k' i' j'] by (metis less_irrefl)
      hence k2k': k2 < k' using kth_obs_mono[OF is_kth_obs π' k' i' ik2] ji' by (metis not_less_iff_gr_or_eq)
      hence k2k: k2 < k using Suc by auto
      from Suc.IH[OF nretj k2k ik2 csj ikj] show False .
    qed
  next
    assume π i = return
    hence reti': π' i' = return by (metis csi last_cs)
    from ret_obs_all_obs[OF path(2) ik' reti' kk', of False] not_in_π'
    show False by blast
  qed
qed

lemma kth_obs_cs_missing_cs:  assumes path: is_path π is_path π' and iki: is_kth_obs π k i and iki': is_kth_obs π' k i' and csi: ‹cs⇗πi  cs⇗π'i' 
obtains l j where j  i is_kth_obs π l j ¬ ( j'. cs⇗πj = cs⇗π'j') | l' j' where j'  i' is_kth_obs π' l' j' ¬ ( j. cs⇗πj = cs⇗π'j')
proof (rule ccontr)
  assume nt: ¬ thesis 
  show False using iki iki' csi that proof (induction k arbitrary: i i' rule: less_induct)
    case (less k i i')
    hence all_in_π':  l j. ji  is_kth_obs π l j  ( j' . cs⇗πj = cs⇗π'j') 
    and all_in_π:  l' j'. j'  i'  is_kth_obs π' l' j'  ( j . cs⇗πj = cs⇗π'j') by (metis nt) (metis nt less(6))
    obtain j j' where csji: ‹cs⇗πj = cs⇗π'i' and csij: ‹cs⇗πi = cs⇗π'j' using all_in_π all_in_π' less by blast 
    then obtain l l' where ilj: is_kth_obs π l j and ilj': is_kth_obs π' l' j' by (metis is_kth_obs_def last_cs less.prems(1,2))
    have lnk: l  k using ilj csji less(2) less(4) kth_obs_unique by auto
    have lnk': l'  k using ilj' csij less(3) less(4) kth_obs_unique by auto
    have cseq:  l j j'. l < k   is_kth_obs π l j  is_kth_obs π' l j'  cs⇗πj = cs⇗π'j' proof - 
      { fix t p p' assume tk: t < k and ikp: is_kth_obs π t p and ikp': is_kth_obs π' t p' 
        hence pi: p < i and pi': p' < i' by (metis kth_obs_mono less.prems(1)) (metis kth_obs_mono less.prems(2) tk ikp') 
        have *: j l. j  p  is_kth_obs π l j  j'. cs⇗πj = cs⇗π'j' using pi all_in_π' by auto
        have **: j' l'. j'  p'  is_kth_obs π' l' j'  j. cs⇗πj = cs⇗π'j' using pi' all_in_π by auto
        have ‹cs⇗πp = cs⇗π'p' apply(rule ccontr) using less(1)[OF tk ikp ikp'] * ** by blast
      }
      thus ?thesis by blast
    qed
    have ii'nret: π i  return  π' i'  return using less cs_return by auto
    have a: k < l  k < l' proof (rule ccontr)
      assume ¬(k < l  k < l') 
      hence *: l < k l' < k using lnk lnk' by auto
      hence ji: j < i and ji': j' < i' using ilj ilj' less(2,3) kth_obs_mono by auto      
      show False using ii'nret proof
        assume nreti: π i  return
        hence nretj': π' j'  return using last_cs csij by metis
        show False using cs_order[OF path(2,1) csij[symmetric] csji[symmetric] nretj' ji'] ji by simp
      next
        assume nreti': π' i'  return
        hence nretj': π j  return using last_cs csji by metis
        show False using cs_order[OF path csji csij nretj' ji] ji' by simp
      qed
    qed
    have l < k  l' < k proof (rule ccontr)
      assume ¬ (l< k  l' < k)
      hence k < l k < l' using lnk lnk' by auto
      hence ji: i < j and ji': i' < j' using ilj ilj' less(2,3) kth_obs_mono by auto
      show False using ii'nret proof
        assume nreti: π i  return
        show False using cs_order[OF path csij csji nreti ji]  ji' by simp
      next
        assume nreti': π' i'  return
        show False using cs_order[OF path(2,1) csji[symmetric] csij[symmetric] nreti' ji'] ji by simp
      qed
    qed    
    hence k < l  l' < k  k < l'  l < k using a by auto
    thus False proof
      assume k < l  l' < k
      hence kl: k < l and lk': l' < k by auto    
      hence ij: i < j and ji': j' < i' using less(2,3) ilj ilj' kth_obs_mono by auto      
      have nreti: π i  return by (metis csji ii'nret ij last_cs path(1) term_path_stable less_imp_le)
      obtain h where ilh: is_kth_obs π l' h using ji' all_in_π ilj' no_kth_obs_missing_cs path(1) path(2) by (metis kl lk' ilj kth_obs_stable)
      hence ‹cs⇗πh = cs⇗π'j' using cseq lk' ilj' by blast
      hence ‹cs⇗πi = cs⇗πh using csij by auto
      hence hi: h = i using cs_inj nreti path(1) by metis      
      have l' = k using less(2) ilh unfolding hi by (metis is_kth_obs_def)      
      thus False using lk' by simp
    next
      assume k < l'  l < k
      hence kl': k < l' and lk: l < k by auto    
      hence ij': i' < j' and ji: j < i using less(2,3) ilj ilj' kth_obs_mono by auto      
      have nreti': π' i'  return by (metis csij ii'nret ij' last_cs path(2) term_path_stable less_imp_le)
      obtain h' where ilh': is_kth_obs π' l h' using all_in_π' ilj no_kth_obs_missing_cs path(1) path(2) kl' lk ilj' kth_obs_stable by metis
      hence ‹cs⇗πj = cs⇗π'h' using cseq lk ilj by blast
      hence ‹cs⇗π'i' = cs⇗π'h' using csji by auto
      hence hi: h' = i' using cs_inj nreti' path(2) by metis      
      have l = k using less(3) ilh' unfolding hi by (metis is_kth_obs_def)      
      thus False using lk by simp
    qed
  qed
qed


subsection ‹Facts about Data›

lemma reads_restrict1: σ  (reads n) = σ'  (reads n)   x  reads n. σ x = σ' x by (metis restrict_def)

lemma reads_restrict2:  x  reads n. σ x = σ' x  σ  (reads n) = σ'  (reads n)  unfolding restrict_def by auto

lemma reads_restrict: (σ  (reads n) = σ'  (reads n)) = ( x  reads n. σ x = σ' x) using reads_restrict1 reads_restrict2 by metis

lemma reads_restr_suc: σ  (reads n) = σ'  (reads n)  suc n σ = suc n σ' by (metis reads_restrict uses_suc)

lemma reads_restr_sem: σ  (reads n) = σ'  (reads n)   v  writes n. sem n σ v = sem n σ' v by (metis reads_restrict1 uses_writes)

lemma reads_obsp: assumes path σ k = path σ' k' σk (reads (path σ k)) = σ'k' (reads (path σ k)) shows obsp σ k = obsp σ' k' 
  using assms(2) uses_att 
  unfolding obsp_def assms(1) reads_restrict 
  apply (cases att (path σ' k'))  
  by auto

lemma no_writes_unchanged0: assumes  l<k. v writes(path σ l) shows (σk) v = σ v using assms 
proof (induction k)
  case 0 thus ?case by(auto simp add: kth_state_def) 
next
  case (Suc k)
  hence (σk) v = σ v by auto
  moreover 
  have σSuc k= snd ( step (path σ k,σk)) by (metis kth_state_suc)
  hence σSuc k= sem (path σ k) (σk) by (metis step_suc_sem snd_conv)
  moreover
  have v  writes (path σ k) using Suc.prems by blast
  ultimately 
  show ?case using writes by metis
qed

lemma written_read_dd: assumes is_path π v  reads (π k) v  writes (π j) j<k obtains l where k dd⇗π,v⇖→ l 
proof -
  let ?l = GREATEST l. l < k  v  writes (π l)
  have ?l < k by (metis (no_types, lifting) GreatestI_ex_nat assms(3) assms(4) less_or_eq_imp_le)
  moreover
  have v  writes (π ?l) by (metis (no_types, lifting) GreatestI_nat assms(3) assms(4) less_or_eq_imp_le) 
  hence v  reads (π k)  writes (π ?l) using assms(2) by auto
  moreover
  note is_ddi_def
  have  l  {?l<..<k}. v  writes (π l) by (auto, metis (lifting, no_types) Greatest_le_nat le_antisym nat_less_le)
  ultimately 
  have k dd⇗π,v⇖→ ?l using assms(1) unfolding is_ddi_def by blast
  thus thesis using that by simp
qed

lemma no_writes_unchanged: assumes k  l  j  {k..<l}. v writes(path σ j) shows (σl) v = (σk) v using assms
proof (induction l - k arbitrary: l)
  case 0 thus ?case by(auto) 
next
  case (Suc lk l)
  hence kl: k < l by auto
  then obtain l' where lsuc: l = Suc l' using lessE by blast
  hence lk = l' - k using Suc by auto
  moreover 
  have  j  {k..<l'}. v  writes (path σ j) using Suc(4) lsuc by auto
  ultimately  
  have (σl') v = (σk) v using Suc(1)[of l'] lsuc kl by fastforce
  moreover 
  have σl= snd ( step (path σ l',σl')) by (metis kth_state_suc lsuc)
  hence σl= sem (path σ l') (σl') by (metis step_suc_sem snd_conv)
  moreover
  have l' < l k  l' using kl lsuc by auto
  hence v  writes (path σ l') using Suc.prems(2) by auto
  ultimately 
  show ?case using writes by metis
qed

lemma ddi_value: assumes l dd⇗(path σ),v⇖→ k shows (σl) v = (σSuc k) v
using assms no_writes_unchanged[of Suc k l v σ] unfolding is_ddi_def by auto

lemma written_value: assumes path σ l = path σ' l' σl reads (path σ l) = σ'l' reads (path σ l) v  writes (path σ l) 
shows (σSuc l) v = (σ'Suc l') v 
by (metis assms reads_restr_sem snd_conv step_suc_sem kth_state_suc) 


subsection ‹Facts about Contradicting Paths›

lemma obsp_contradict: assumes csk: ‹cs⇗path σk = cs⇗path σ'k' and obs: obsp σ k  obsp σ' k' shows (σ', k') 𝔠 (σ, k)
proof -
  have pk: path σ k = path σ' k' using assms last_cs by metis
  hence σk(reads (path σ k))  σ'k'(reads (path σ k)) using obs reads_obsp[OF pk] by auto
  thus (σ',k') 𝔠 (σ,k) using contradicts.intros(2)[OF csk[symmetric]] by auto
qed

lemma missing_cs_contradicts: assumes notin: ¬( k'. cs⇗path σk = cs⇗path σ'k') and converge: k<n ‹cs⇗path σn = cs⇗path σ'n' shows  j'. (σ', j') 𝔠 (σ, k)
proof -
  let  = path σ
  let ?π' = path σ'
  have init:  0 = ?π' 0 unfolding path_def by auto
  have path: is_path  is_path ?π' using path_is_path by auto
  obtain j j' where csj: ‹cs⇗j = cs⇗?π'j' and cd: k cd⇗⇖→j and suc:  (Suc j)  ?π' (Suc j') using converged_cd_diverge[OF path init notin converge] .
  have less: ‹cs⇗j  cs⇗k using cd cd_is_cs_less by auto
  have nretj:  j  return by (metis cd is_cdi_def term_path_stable less_imp_le)
  have cs:  ¡ cs⇗?π'j' = j using csj cs_select_id nretj path_is_path by metis
  have (σ',j') 𝔠 (σ,k) using contradicts.intros(1)[of ?π' j'  k σ σ',unfolded cs] less suc csj by metis
  thus ?thesis by blast
qed

theorem obs_neq_contradicts_term: fixes σ σ' defines π: π  path σ and π': π'  path σ' assumes ret: π n = return π' n' = return and obsne: obs σ  obs σ' 
shows  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom (att))  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom (att))
proof - 
  have path: is_path π is_path π' using π π' path_is_path by auto
  obtain k1 where neq: obs σ k1  obs σ' k1 using obsne ext[of obs σ obs σ'] by blast  
  hence (k i i'. is_kth_obs π k i  is_kth_obs π' k i'  obsp σ i  obsp σ' i'  cs⇗πi = cs⇗π'i') 
   ( k i. is_kth_obs π k i  ¬ ( i'. cs⇗πi = cs⇗π'i')) 
   ( k i'. is_kth_obs π' k i'  ¬ ( i. cs⇗πi = cs⇗π'i'))
  proof(cases rule: option_neq_cases)
    case (none2 x)
    have notinπ': ¬ ( l. is_kth_obs π' k1 l) using none2(2) π' obs_none_no_kth_obs by auto
    obtain i where inπ: is_kth_obs π k1 i using obs_some_kth_obs[of σ k1] none2(1) π by auto            
    obtain l j where is_kth_obs π l j ¬ ( j'. cs⇗πj = cs⇗π'j') using path inπ notinπ' by (metis no_kth_obs_missing_cs)
    thus ?thesis by blast
  next
    case (none1 x)
    have notinπ: ¬ ( l. is_kth_obs π k1 l) using none1(1) π obs_none_no_kth_obs by auto
    obtain i' where inπ': is_kth_obs π' k1 i' using obs_some_kth_obs[of σ' k1] none1(2) π' by auto            
    obtain l j where is_kth_obs π' l j ¬ ( j'. cs⇗πj' = cs⇗π'j) using path inπ' notinπ by (metis no_kth_obs_missing_cs)
    thus ?thesis by blast
  next  
    case (some x y)
    obtain i where inπ: is_kth_obs π k1 i using obs_some_kth_obs[of σ k1] some π by auto
    obtain i' where inπ': is_kth_obs π' k1 i' using obs_some_kth_obs[of σ' k1] some π' by auto
    show ?thesis proof (cases)
      assume *: ‹cs⇗πi = cs⇗π'i'
      have obsp σ i = obs σ k1 by (metis obs_def π inπ kth_obs_unique the_equality)
      moreover
      have obsp σ' i' = obs σ' k1 by (metis obs_def π' inπ' kth_obs_unique the_equality)
      ultimately
      have obsp σ i  obsp σ' i' using neq by auto
      thus ?thesis using * inπ inπ' by blast
    next
      assume *: ‹cs⇗πi  cs⇗π'i'
      note kth_obs_cs_missing_cs[OF path inπ inπ' *]
      thus ?thesis by metis
    qed
  qed
  thus ?thesis proof (cases rule: three_cases)
    case 1
    then obtain k i i' where iki: is_kth_obs π k i is_kth_obs π' k i' and obsne: obsp σ i  obsp σ' i' and csi: ‹cs⇗πi = cs⇗π'i' by auto
    note obsp_contradict[OF csi[unfolded π π'] obsne]
    moreover
    have π i  dom att using iki unfolding is_kth_obs_def by auto
    ultimately
    show ?thesis by blast
  next
    case 2
    then obtain k i where iki: is_kth_obs π k i and notinπ': ¬ (i'. cs⇗πi = cs⇗π'i') by auto
    let ?n = Suc (max n i)
    have nn: n < ?n by auto
    have iln: i < ?n by auto
    have retn: π ?n = return using ret term_path_stable path by auto
    hence ‹cs⇗π?n = cs⇗π'n' using ret(2) cs_return by auto
    then obtain i' where (σ',i') 𝔠 (σ,i) using missing_cs_contradicts[OF notinπ'[unfolded π π'] iln] π π' by auto
    moreover
    have π i  dom att using iki is_kth_obs_def by auto
    ultimately
    show ?thesis by blast
  next
    case 3
    then obtain k i' where iki: is_kth_obs π' k i' and notinπ': ¬ (i. cs⇗πi = cs⇗π'i') by auto
    let ?n = Suc (max n' i')
    have nn: n' < ?n by auto
    have iln: i' < ?n by auto
    have retn: π' ?n = return using ret term_path_stable path by auto
    hence ‹cs⇗πn = cs⇗π'?n using ret(1) cs_return by auto
    then obtain i where (σ,i) 𝔠 (σ',i') using missing_cs_contradicts notinπ' iln π π' by metis
    moreover
    have π' i'  dom att using iki is_kth_obs_def by auto
    ultimately
    show ?thesis by blast
  qed
qed

lemma obs_neq_some_contradicts': fixes σ σ' defines π: π  path σ and π': π'  path σ' 
assumes obsnecs: obsp σ i  obsp σ' i'  cs⇗πi  cs⇗π'i'
and iki: is_kth_obs π k i and iki': is_kth_obs π' k i'
shows  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom att)  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom att)
using obsnecs iki iki' proof (induction k arbitrary: i i' rule: less_induct )
  case (less k i i')  
  note iki = is_kth_obs π k i
  and iki' = is_kth_obs π' k i'
  have domi: π i  dom att by (metis is_kth_obs_def domIff iki)
  have domi': π' i'  dom att by (metis is_kth_obs_def domIff iki')
  note obsnecs = obsp σ i  obsp σ' i'  cs⇗πi  cs⇗π'i'  
  show ?thesis proof cases
    assume csi: ‹cs⇗πi = cs⇗π'i'
    hence *: obsp σ i  obsp σ' i' using obsnecs by auto
    note obsp_contradict[OF _ *] csi domi π π'
    thus ?thesis by blast    
  next      
    assume ncsi: ‹cs⇗πi  cs⇗π'i'  
    have path: is_path π is_path π' using π π' path_is_path by auto
    have π0: π 0 = π' 0 unfolding π π' path_def by auto
    note kth_obs_cs_missing_cs[of π π' k i i'] π π' path_is_path iki iki' ncsi 
    hence ( l j .j  i  is_kth_obs π l j  ¬ ( j'. cs⇗πj = cs⇗π'j'))  ( l' j'. j'  i'  is_kth_obs π' l' j'  ¬ ( j. cs⇗πj = cs⇗π'j')) by metis
    thus ?thesis proof
      assume l j. j  i  is_kth_obs π l j  ¬ (j'. cs⇗πj = cs⇗π'j')
      then obtain l j where ji: ji and iobs: is_kth_obs π l j and notin: ¬ (j'. cs⇗πj = cs⇗π'j') by blast
      have dom: π j  dom att using iobs is_kth_obs_def by auto
      obtain n n' where nj: n < j and csn: ‹cs⇗πn = cs⇗π'n' and sucn:  π (Suc n)  π' (Suc n') and cdloop: j cd⇗π⇖→ n  ( j'> n'. j' cd⇗π'⇖→ n')
      using missing_cd_or_loop[OF path π0 notin] by blast
      show ?thesis using cdloop proof
        assume cdjn: j cd⇗π⇖→ n
        hence csnj: ‹cs⇗π'n'  cs⇗πj using csn by (metis cd_is_cs_less)
        have cssel: π (Suc (π ¡ cs⇗π'n')) = π (Suc n) using csn by (metis cdjn cd_not_ret cs_select_id path(1))
        have (σ',n') 𝔠 (σ,j) using csnj apply(rule contradicts.intros(1)) using cssel π π' sucn by auto 
        thus ?thesis using dom by auto
      next
        assume loop:  j'>n'. j' cd⇗π'⇖→ n'
        show ?thesis proof cases
          assume in': i'  n'
          have nreti': π' i'  return by( metis le_eq_less_or_eq lessI loop not_le path(2) ret_no_cd term_path_stable)
          show ?thesis proof cases
            assume  ι. cs⇗π'i' = cs⇗πι
            then obtain ι where csι: ‹cs⇗πι = cs⇗π'i' by metis            
            have ιn: ι  n using cs_order_le[OF path(2,1) csι[symmetric] csn[symmetric] nreti' in'] .
            hence ιi: ι < i using nj ji by auto 
            have domι: π ι  dom att using domi' csι last_cs by metis
            obtain κ where iκι: is_kth_obs π κ ι using domι by (metis is_kth_obs_def domIff)
            hence κk: κ < k using ιi iki by (metis kth_obs_le_iff)
            obtain ι' where iκι': is_kth_obs π' κ ι' using κk iki' by (metis kth_obs_stable)
            have ι' < i' using κk iki' iκι' by (metis kth_obs_le_iff)
            hence csι': ‹cs⇗πι  cs⇗π'ι' unfolding csι using cs_inj[OF path(2) nreti', of ι'] by blast           
            thus ?thesis using less(1)[OF κk _ iκι iκι'] by auto
          next
            assume notin'': ¬( ι. cs⇗π'i' = cs⇗πι)
            obtain ι ι' where ιi': ι' < i' and csι: ‹cs⇗πι = cs⇗π'ι' and sucι: π (Suc ι)  π' (Suc ι') and cdloop': i' cd⇗π'⇖→ ι'  ( j>ι. j cd⇗π⇖→ ι)
            using missing_cd_or_loop[OF path(2,1) π0[symmetric] notin''] by metis
            show ?thesis using cdloop' proof
              assume cdjn: i' cd⇗π'⇖→ ι'
              hence csnj: ‹cs⇗πι  cs⇗π'i' using csι by (metis cd_is_cs_less)
              have cssel: π' (Suc (π' ¡ cs⇗πι)) = π' (Suc ι') using csι by (metis cdjn cd_not_ret cs_select_id path(2))
              have (σ,ι) 𝔠 (σ',i') using csnj apply(rule contradicts.intros(1)) using cssel π π' sucι by auto 
              thus ?thesis using domi' by auto
            next
              assume loop':  j>ι. j cd⇗π⇖→ ι
              have ιn': ι' < n' using in' ιi' by auto
              have nretι': π' ι'  return by (metis csι last_cs le_eq_less_or_eq lessI path(1) path(2) sucι term_path_stable)
              have ι < n using cs_order[OF path(2,1) csι[symmetric] csn[symmetric] nretι' ιn'] .
              hence ι < i using nj ji by auto
              hence cdiι: i cd⇗π⇖→ ι using loop' by auto
              hence csιi: ‹cs⇗π'ι'  cs⇗πi using csι by (metis cd_is_cs_less)
              have cssel: π (Suc (π ¡ cs⇗π'ι')) = π (Suc ι) using csι by (metis cdiι cd_not_ret cs_select_id path(1))
              have (σ',ι') 𝔠 (σ,i) using csιi apply(rule contradicts.intros(1)) using cssel π π' sucι by auto 
              thus ?thesis using domi by auto
            qed
          qed
        next
          assume ¬ i'  n'
          hence ni': n'< i' by simp
          hence cdin: i' cd⇗π'⇖→ n' using loop by auto
          hence csni: ‹cs⇗πn  cs⇗π'i' using csn by (metis cd_is_cs_less)
          have cssel: π' (Suc (π' ¡ cs⇗πn)) = π' (Suc n') using csn by (metis cdin cd_not_ret cs_select_id path(2))
          have (σ,n) 𝔠 (σ',i') using csni apply(rule contradicts.intros(1)) using cssel π π' sucn by auto 
          thus ?thesis using domi' by auto
        qed
      qed
    next
      ― ‹Symmetric case as above, indices might be messy.›
      assume l j. j  i'  is_kth_obs π' l j  ¬ (j'. cs⇗πj' = cs⇗π'j)
      then obtain l j where ji': ji' and iobs: is_kth_obs π' l j and notin: ¬ (j'. cs⇗π'j = cs⇗πj') by metis
      have dom: π' j  dom att using iobs is_kth_obs_def by auto
      obtain n n' where nj: n < j and csn: ‹cs⇗π'n = cs⇗πn' and sucn:  π' (Suc n)  π (Suc n') and cdloop: j cd⇗π'⇖→ n  ( j'> n'. j' cd⇗π⇖→ n')
      using missing_cd_or_loop[OF path(2,1) π0[symmetric] ] notin by metis
      show ?thesis using cdloop proof
        assume cdjn: j cd⇗π'⇖→ n
        hence csnj: ‹cs⇗πn'  cs⇗π'j using csn by (metis cd_is_cs_less)
        have cssel: π' (Suc (π' ¡ cs⇗πn')) = π' (Suc n) using csn by (metis cdjn cd_not_ret cs_select_id path(2))
        have (σ,n') 𝔠 (σ',j) using csnj apply(rule contradicts.intros(1)) using cssel π' π sucn by auto 
        thus ?thesis using dom by auto
      next
        assume loop:  j'>n'. j' cd⇗π⇖→ n'
        show ?thesis proof cases
          assume in': i  n'
          have nreti: π i  return by (metis le_eq_less_or_eq lessI loop not_le path(1) ret_no_cd term_path_stable)
          show ?thesis proof cases
            assume  ι. cs⇗πi = cs⇗π'ι
            then obtain ι where csι: ‹cs⇗π'ι = cs⇗πi by metis            
            have ιn: ι  n using cs_order_le[OF path csι[symmetric] csn[symmetric] nreti in'] .
            hence ιi': ι < i' using nj ji' by auto 
            have domι: π' ι  dom att using domi csι last_cs by metis
            obtain κ where iκι: is_kth_obs π' κ ι using domι by (metis is_kth_obs_def domIff)
            hence κk: κ < k using ιi' iki' by (metis kth_obs_le_iff)
            obtain ι' where iκι': is_kth_obs π κ ι' using κk iki by (metis kth_obs_stable)
            have ι' < i using κk iki iκι' by (metis kth_obs_le_iff)
            hence csι': ‹cs⇗π'ι  cs⇗πι' unfolding csι using cs_inj[OF path(1) nreti, of ι'] by blast           
            thus ?thesis using less(1)[OF κk _ iκι' iκι] by auto
          next
            assume notin'': ¬( ι. cs⇗πi = cs⇗π'ι)
            obtain ι ι' where ιi: ι' < i and csι: ‹cs⇗π'ι = cs⇗πι' and sucι: π' (Suc ι)  π (Suc ι') and cdloop': i cd⇗π⇖→ ι'  ( j>ι. j cd⇗π'⇖→ ι)
            using missing_cd_or_loop[OF path π0 notin''] by metis
            show ?thesis using cdloop' proof
              assume cdjn: i cd⇗π⇖→ ι'
              hence csnj: ‹cs⇗π'ι  cs⇗πi using csι by (metis cd_is_cs_less)
              have cssel: π (Suc (π ¡ cs⇗π'ι)) = π (Suc ι') using csι by (metis cdjn cd_not_ret cs_select_id path(1))
              have (σ',ι) 𝔠 (σ,i) using csnj apply(rule contradicts.intros(1)) using cssel π' π sucι by auto 
              thus ?thesis using domi by auto
            next
              assume loop':  j>ι. j cd⇗π'⇖→ ι
              have ιn': ι' < n' using in' ιi by auto
              have nretι': π ι'  return by (metis csι last_cs le_eq_less_or_eq lessI path(1) path(2) sucι term_path_stable)
              have ι < n using cs_order[OF path csι[symmetric] csn[symmetric] nretι' ιn'] .
              hence ι < i' using nj ji' by auto
              hence cdiι: i' cd⇗π'⇖→ ι using loop' by auto
              hence csιi': ‹cs⇗πι'  cs⇗π'i' using csι by (metis cd_is_cs_less)
              have cssel: π' (Suc (π' ¡ cs⇗πι')) = π' (Suc ι) using csι by (metis cdiι cd_not_ret cs_select_id path(2))
              have (σ,ι') 𝔠 (σ',i') using csιi' apply(rule contradicts.intros(1)) using cssel π' π sucι by auto 
              thus ?thesis using domi' by auto
            qed
          qed
        next
          assume ¬ i  n'
          hence ni: n'< i by simp
          hence cdin: i cd⇗π⇖→ n' using loop by auto
          hence csni': ‹cs⇗π'n  cs⇗πi using csn by (metis cd_is_cs_less)
          have cssel: π (Suc (π ¡ cs⇗π'n)) = π (Suc n') using csn by (metis cdin cd_not_ret cs_select_id path(1))
          have (σ',n) 𝔠 (σ,i) using csni' apply(rule contradicts.intros(1)) using cssel π' π sucn by auto 
          thus ?thesis using domi by auto
        qed
      qed
    qed
  qed
qed

theorem obs_neq_some_contradicts: fixes σ σ' defines π: π  path σ and π': π'  path σ' 
assumes obsne: obs σ k  obs σ' k and not_none: obs σ k  None obs σ' k  None 
shows  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom att)  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom att)
proof -
  obtain i where iki: is_kth_obs π k i using not_none(1) by (metis π obs_some_kth_obs)
  obtain i' where iki': is_kth_obs π' k i' using not_none(2) by (metis π' obs_some_kth_obs)
  have obsp σ i = obs σ k by (metis π iki kth_obs_unique obs_def the_equality)
  moreover
  have obsp σ' i' = obs σ' k by (metis π' iki' kth_obs_unique obs_def the_equality)
  ultimately
  have obspne: obsp σ i  obsp σ' i' using obsne by auto
  show ?thesis using obs_neq_some_contradicts'[OF _ iki[unfolded π] iki'[unfolded π']] using obspne π π' by metis
qed

theorem obs_neq_ret_contradicts: fixes σ σ' defines π: π  path σ and π': π'  path σ' 
assumes ret: π n = return and obsne: obs σ' i  obs σ i and obs:obs σ' i  None
shows  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom (att))  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom (att))
proof (cases  j k'. is_kth_obs π' j k'  ( k. cs⇗πk = cs⇗π'k'))
  case True
  obtain l k' where jk': is_kth_obs π' l k' and unmatched: ( k. cs⇗πk = cs⇗π'k') using True by blast
  have π0: π 0 = π' 0 using π π' path0 by auto
  obtain j j' where csj: ‹cs⇗πj = cs⇗π'j' and cd: k' cd⇗π'⇖→j' and suc: π (Suc j)  π' (Suc j')
    using converged_cd_diverge_return[of π' π k' n] ret unmatched path_is_path π π' π0 by metis 
  hence *: (σ, j) 𝔠 (σ' ,k') using contradicts.intros(1)[of π j π' k' σ' σ, unfolded csj] π π'
    using cd_is_cs_less cd_not_ret cs_select_id by auto 
  have π' k'  dom(att) using jk' by (meson domIff is_kth_obs_def) 
  thus ?thesis using * by blast
next
  case False
  hence *:  j k'. is_kth_obs π' j k'   k. cs⇗πk = cs⇗π'k' by auto
  obtain k' where k': is_kth_obs π' i k' using obs π' obs_some_kth_obs by blast
  obtain l where is_kth_obs π i l using * π π' k' no_kth_obs_missing_cs path_is_path by metis
  thus ?thesis using π π' obs obs_neq_some_contradicts obs_none_no_kth_obs obsne by metis
qed


subsection ‹Facts about Critical Observable Paths›

lemma contradicting_in_cp: assumes leq:σ =L σ' and cseq: ‹cs⇗path σk = cs⇗path σ'k' 
and readv: vreads(path σ k) and vneq: (σk) v  (σ'k') v shows ((σ,k),(σ',k'))  cp
  using cseq readv vneq proof(induction k+k' arbitrary: k k' v rule: less_induct)
  fix k k' v     
  assume csk: ‹cs⇗path σk = cs⇗path σ'k'
  assume vread: v  reads (path σ k)
  assume vneq: (σk) v  (σ'k') v
  assume IH: ka k'a v. ka + k'a < k + k'  cs⇗path σka = cs⇗path σ'k'a  v  reads (path σ ka)  (σka) v  (σ'k'a) v  ((σ, ka), σ', k'a)  cp 
  
  define π where  π  path σ 
  define π' where π'  path σ' 
  have path: π = path σ π' = path σ' using π_def π'_def path_is_path by auto  
  have ip: is_path π is_path π' using path path_is_path by auto
            
  have π0: π' 0 = π 0 unfolding path path_def by auto
  have vread': v  reads (path σ' k') using csk vread by (metis last_cs)
  have cseq: ‹cs⇗π'k' = cs⇗πk using csk path by simp
  
  show ((σ, k), σ', k')  cp proof cases
    assume vnw:  l < k. vwrites (π l)
    hence σv: (σk) v = σ v by (metis no_writes_unchanged0 path(1))
    show ?thesis proof cases
      assume vnw':  l < k'. vwrites (π' l)
      hence σv': (σ'k') v = σ' v by (metis no_writes_unchanged0 path(2))
      with σv vneq have σ v  σ' v by auto
      hence vhigh: v  hvars using leq unfolding loweq_def restrict_def by (auto,metis)
      thus ?thesis using cp.intros(1)[OF leq csk vread vneq] vnw vnw' path by simp
    next
      assume ¬( l < k'. vwrites (π' l))
      then obtain l' where kddl': k' dd⇗π',v⇖→ l' using path(2) path_is_path written_read_dd vread' by blast
      hence lv': v  writes (π' l') unfolding is_ddi_def by auto
      have lk': l' < k' by (metis is_ddi_def kddl')
      have nret: π' l'  return using lv' writes_return by auto
      
      have notinπ: ¬ (l. cs⇗π'l' = cs⇗πl) proof
        assume l. cs⇗π'l' = cs⇗πl
        then obtain l where "cs⇗π'l' = cs⇗πl" ..
        note csl = ‹cs⇗π'l' = cs⇗πl
        have lk: l < k using lk' cseq ip cs_order[of π' π l' l k' k] csl nret path by force
                  
        have v  writes (π l) using csl lv' last_cs by metis
        thus False using lk vnw by blast
      qed

      from converged_cd_diverge[OF ip(2,1) π0 notinπ lk' cseq]
      obtain i i' where  csi: ‹cs⇗π'i' = cs⇗πi and lcdi: l' cd⇗π'⇖→ i'  and div: π' (Suc i')  π (Suc i) .
      
      have 1: π (Suc i) = suc (π i) (σi) by (metis step_suc_sem fst_conv path(1) path_suc)
      have 2: π' (Suc i') = suc (π' i') (σ'i') by (metis step_suc_sem fst_conv path(2) path_suc)
      have 3: π' i' = π i using csi last_cs by metis
      have nreads: σi reads (π i)  σ'i' reads (π i) by (metis 1 2 3 div reads_restr_suc)
      then obtain v' where v'read: v' reads(path σ i) (σi) v'  (σ'i') v' unfolding path by (metis reads_restrict)
      
      have nreti: π' i'  return by (metis csi div ip(1) ip(2) last_cs lessI term_path_stable less_imp_le)
      have ik': i' < k' using lcdi lk' is_cdi_def by auto            
      have ik: i < k using cs_order[OF ip(2,1) csi cseq nreti ik'] .
      
      have cpi: ((σ, i), (σ', i'))  cp using IH[of i i'] v'read csi ik ik' path by auto 
      hence cpi': ((σ', i'), (σ, i))  cp using cp.intros(4) by blast
      
      have nwvi: j'{LEAST i'. i < i'  (i. cs⇗path σ'i = cs⇗path σi')..<k}. v  writes (path σ j') using vnw[unfolded path] 
        by (metis (poly_guards_query) atLeastLessThan_iff)
      
      from cp.intros(3)[OF cpi' kddl'[unfolded path] lcdi[unfolded path] csk[symmetric] div[unfolded path] vneq[symmetric] nwvi] 
      
      show ?thesis using cp.intros(4) by simp 
    qed
  next
    assume wv: ¬ ( l<k. v  writes (π l)) 
    then obtain l where kddl: k dd⇗π,v⇖→ l using path(1) path_is_path written_read_dd vread by blast
    hence lv: v  writes (π l) unfolding is_ddi_def by auto
    have lk: l < k by (metis is_ddi_def kddl)
    have nret: π l  return using lv writes_return by auto
    have nwb:  i  {Suc l..< k}. vwrites(π i) using kddl unfolding is_ddi_def by auto
    have σvk: (σk) v = (σSuc l) v using kddl ddi_value path(1) by auto

    show ?thesis proof cases
      assume vnw':  l < k'. vwrites (π' l)
      hence σv': (σ'k') v = σ' v by (metis no_writes_unchanged0 path(2))

      have notinπ': ¬ (l'. cs⇗πl = cs⇗π'l') proof
        assume l'. cs⇗πl = cs⇗π'l'
        then obtain l' where "cs⇗πl = cs⇗π'l'" ..
        note csl = ‹cs⇗πl = cs⇗π'l'
        have lk: l' < k' using lk cseq ip cs_order[of π π' l l' k k'] csl nret by metis
                  
        have v  writes (π' l') using csl lv last_cs by metis
        thus False using lk vnw' by blast
      qed

      from converged_cd_diverge[OF ip(1,2) π0[symmetric] notinπ' lk cseq[symmetric]]
      obtain i i' where  csi: ‹cs⇗π'i' = cs⇗πi and lcdi: l cd⇗π⇖→ i  and div: π (Suc i)  π' (Suc i') by metis
      
      have 1: π (Suc i) = suc (π i) (σi) by (metis step_suc_sem fst_conv path(1) path_suc)
      have 2: π' (Suc i') = suc (π' i') (σ'i') by (metis step_suc_sem fst_conv path(2) path_suc)
      have 3: π' i' = π i using csi last_cs by metis
      have nreads: σi reads (π i)  σ'i' reads (π i) by (metis 1 2 3 div reads_restr_suc)
      have contri: (σ',i') 𝔠 (σ,i) using contradicts.intros(2)[OF csi path nreads] .
      
      have nreti: π i  return by (metis csi div ip(1) ip(2) last_cs lessI term_path_stable less_imp_le)
      have ik: i < k using lcdi lk is_cdi_def by auto            
      have ik': i' < k' using cs_order[OF ip(1,2) csi[symmetric] cseq[symmetric] nreti ik] .
      have nreads: σi reads (π i)  σ'i' reads (π i) by (metis 1 2 3 div reads_restr_suc)
      then obtain v' where v'read: v' reads(path σ i) (σi) v'  (σ'i') v' unfolding path by (metis reads_restrict)
      
      
      have cpi: ((σ, i), (σ', i'))  cp using IH[of i i'] v'read csi ik ik' path by auto 
      hence cpi': ((σ', i'), (σ, i))  cp using cp.intros(4) by blast
      
      have vnwi: j'{LEAST i'a. i' < i'a  (i. cs⇗path σi = cs⇗path σ'i'a)..<k'}. v  writes (path σ' j') using vnw'[unfolded path]
        by (metis (poly_guards_query) atLeastLessThan_iff)
        
      from cp.intros(3)[OF cpi kddl[unfolded path] lcdi[unfolded path] csk div[unfolded path] vneq vnwi]   
      
      show ?thesis using cp.intros(4) by simp
    next
      assume ¬ ( l<k'. v  writes (π' l))
      then obtain l' where kddl': k' dd⇗π',v⇖→ l' using path(2) path_is_path written_read_dd vread' by blast
      hence lv': v  writes (π' l') unfolding is_ddi_def by auto
      have lk': l' < k' by (metis is_ddi_def kddl')            
      have nretl': π' l'  return using lv' writes_return by auto
      have nwb':  i'  {Suc l'..< k'}. vwrites(π' i') using kddl' unfolding is_ddi_def by auto
      have σvk': (σ'k') v = (σ'Suc l') v using kddl' ddi_value path(2) by auto

      show ?thesis proof cases 
        assume csl: ‹cs⇗πl = cs⇗π'l'
        hence πl: π l = π' l' by (metis last_cs)
        have σvls: (σSuc l) v  (σ'Suc l') v by (metis σvk σvk' vneq)
        have : σl reads (π l)  σ'l' reads (π l) using path πl σvls written_value lv by blast
        then obtain v' where v'read: v' reads(path σ l) (σl) v'  (σ'l') v' unfolding path by (metis reads_restrict)
      
      
        have cpl: ((σ, l), (σ', l'))  cp using IH[of l l'] v'read csl lk lk' path by auto 
        show ((σ, k), (σ', k'))  cp using cp.intros(2)[OF cpl kddl[unfolded path] kddl'[unfolded path] csk vneq] .        
      next
        assume csl: ‹cs⇗πl  cs⇗π'l'
        show ?thesis proof cases
          assume  i'. cs⇗πl = cs⇗π'i'
          then obtain i' where csli': ‹cs⇗πl = cs⇗π'i' by blast
          have ilne': i'  l' using csl csli' by auto
          have ij': i' < k' using cs_order[OF ip csli' cseq[symmetric] nret lk] .
          have iv': v  writes(π' i') using lv csli' last_cs by metis
          have il': i' < l' using kddl' ilne' ij' iv' unfolding is_ddi_def by auto
          have nreti': π' i'  return using csli' nret last_cs by metis

          have l'notinπ: ¬(i. cs⇗π'l' = cs⇗πi ) proof
            assume i. cs⇗π'l' = cs⇗πi
            then obtain i where csil: ‹cs⇗πi = cs⇗π'l' by metis
            have ik: i < k using cs_order[OF ip(2,1) csil[symmetric] cseq nretl' lk'] .
            have li: l < i using cs_order[OF ip(2,1) csli'[symmetric] csil[symmetric] nreti' il'] .
            have iv: v  writes(π i) using lv' csil last_cs by metis
            show False using kddl ik li iv is_ddi_def by auto
          qed
          
          obtain n n' where csn: ‹cs⇗πn = cs⇗π'n' and lcdn': l' cd⇗π'⇖→ n'  and sucn: π (Suc n)  π' (Suc n') and in': i'  n'
          using converged_cd_diverge_cs [OF ip(2,1) csli'[symmetric] il' l'notinπ lk' cseq] by metis 
          
          ― ‹Can apply the IH to n and n'›
          
          have 1: π (Suc n) = suc (π n) (σn) by (metis step_suc_sem fst_conv path(1) path_suc)
          have 2: π' (Suc n') = suc (π' n') (σ'n') by (metis step_suc_sem fst_conv path(2) path_suc)
          have 3: π' n' = π n using csn last_cs by metis
          have nreads: σn reads (π n)  σ'n' reads (π n) by (metis 1 2 3 sucn reads_restr_suc)
          then obtain v' where v'read: v'reads (path σ n) (σn) v'  (σ'n') v' by (metis path(1) reads_restrict)
          moreover
          have nl': n' < l' using lcdn' is_cdi_def by auto
          have nk': n' < k' using nl' lk' by simp
          have nretn': π' n'  return by (metis ip(2) nl' nretl' term_path_stable less_imp_le)
          have nk: n < k using cs_order[OF ip(2,1) csn[symmetric] cseq nretn' nk'] .
          hence lenn: n+n' < k+k' using nk' by auto
          ultimately  
          have ((σ, n), (σ', n'))  cp using IH csn path by auto
          hence ncp: ((σ', n'), (σ, n))  cp using cp.intros(4) by auto
          
          have nles: n < (LEAST i'. n < i'  (i. cs⇗π'i = cs⇗πi')) (is _ < (LEAST i. ?P i)) using nk cseq LeastI[of ?P k] by metis
          moreover
          have ln: l  n using cs_order_le[OF ip(2,1) csli'[symmetric] csn[symmetric] nreti' in'] .
          ultimately 
          have lles: Suc l  (LEAST i'. n < i'  (i. cs⇗π'i = cs⇗πi')) by auto
          
          have nwcseq: j'{LEAST i'. n < i'  (i. cs⇗π'i = cs⇗πi')..<k}. v  writes (π j') proof 
            fix j' assume *: j'  {LEAST i'. n < i'  (i. cs⇗π'i = cs⇗πi')..<k}
            hence (LEAST i'. n < i'  (i. cs⇗π'i = cs⇗πi'))  j' by (metis (poly_guards_query) atLeastLessThan_iff)
            hence Suc l  j' using lles by auto
            moreover
            have j' < k using * by (metis (poly_guards_query) atLeastLessThan_iff) 
            ultimately have j' {Suc l..<k} by (metis (poly_guards_query) atLeastLessThan_iff)
            thus vwrites (π j') using nwb by auto
          qed
          
          from cp.intros(3)[OF ncp,folded path,OF kddl' lcdn' cseq sucn[symmetric] vneq[symmetric] nwcseq]
          have ((σ', k'), σ, k)  cp .
          thus ((σ, k), (σ', k'))  cp using cp.intros(4) by auto
        next
          assume lnotinπ': ¬ (i'. cs⇗πl = cs⇗π'i')
          show ?thesis proof cases
            assume  i. cs⇗πi = cs⇗π'l'
            then obtain i where csli: ‹cs⇗πi = cs⇗π'l' by blast
            have ilne: i  l using csl csli by auto
            have ij: i < k using cs_order[OF ip(2,1) csli[symmetric] cseq nretl' lk'] .
            have iv: v  writes(π i) using lv' csli last_cs by metis
            have il: i < l using kddl ilne ij iv unfolding is_ddi_def by auto
            have nreti: π i  return using csli nretl' last_cs by metis

            obtain n n' where csn: ‹cs⇗πn = cs⇗π'n' and lcdn: l cd⇗π⇖→ n  and sucn: π (Suc n)  π' (Suc n') and ilen: i  n
            using converged_cd_diverge_cs [OF ip csli il lnotinπ' lk cseq[symmetric]] by metis 
          
            ― ‹Can apply the IH to n and n'›
          
            have 1: π (Suc n) = suc (π n) (σn) by (metis step_suc_sem fst_conv path(1) path_suc)
            have 2: π' (Suc n') = suc (π' n') (σ'n') by (metis step_suc_sem fst_conv path(2) path_suc)
            have 3: π' n' = π n using csn last_cs by metis
            have nreads: σn reads (π n)  σ'n' reads (π n) by (metis 1 2 3 sucn reads_restr_suc)
            then obtain v' where v'read: v'reads (path σ n) (σn) v'  (σ'n') v' by (metis path(1) reads_restrict)
            moreover  
            have nl: n < l using lcdn is_cdi_def by auto
            have nk: n < k using nl lk by simp
            have nretn: π n  return by (metis ip(1) nl nret term_path_stable less_imp_le)
            have nk': n' < k' using cs_order[OF ip csn cseq[symmetric] nretn nk] .
            hence lenn: n+n' < k+k' using nk by auto
            ultimately  
            have ncp: ((σ, n), (σ', n'))  cp using IH csn path by auto
            
            have nles': n' < (LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')) (is _ < (LEAST i. ?P i)) using nk' cseq LeastI[of ?P k'] by metis
            moreover
            have ln': l'  n' using cs_order_le[OF ip csli csn nreti ilen] .
            ultimately 
            have lles': Suc l'  (LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')) by auto
          
            have nwcseq': j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}. v  writes (π' j') proof 
              fix j' assume *: j'  {(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}
              hence (LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))  j' by (metis (poly_guards_query) atLeastLessThan_iff)
              hence Suc l'  j' using lles' by auto
              moreover
              have j' < k' using * by (metis (poly_guards_query) atLeastLessThan_iff) 
              ultimately have j' {Suc l'..<k'} by (metis (poly_guards_query) atLeastLessThan_iff)
              thus vwrites (π' j') using nwb' by auto
              qed
            
            from cp.intros(3)[OF ncp,folded path, OF kddl lcdn cseq[symmetric] sucn vneq nwcseq']
            
            show ((σ, k), (σ', k'))  cp .
          next
            assume l'notinπ: ¬ (i. cs⇗πi = cs⇗π'l')
            define m where m  0::nat
            define m' where m'  0::nat
            have csm: ‹cs⇗πm = cs⇗π'm' unfolding m_def m'_def cs_0 by (metis π0)
            have ml: m<l  m'<l' using csm csl unfolding m_def m'_def by (metis neq0_conv)
            have  n n'. cs⇗πn = cs⇗π'n'  π (Suc n)  π' (Suc n')  
            (l cd⇗π⇖→ n  (j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}. vwrites (π' j'))
             l' cd⇗π'⇖→ n'  (j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j)))
            using csm ml proof (induction k+k'-(m+m') arbitrary: m m' rule: less_induct)
              case (less m m')
              note csm = ‹cs⇗πm = cs⇗π'm'
              note lm = m < l  m' < l'
              note IH =  n n'. 
                k + k' - (n + n') < k + k' - (m + m') 
                cs⇗πn = cs⇗π'n' 
                n < l  n' < l'  ?thesis
              show ?thesis using lm proof
                assume ml: m < l
                obtain n n' where mn: m  n and csn: ‹ cs⇗πn = cs⇗π'n' and lcdn: l cd⇗π⇖→ n and suc: π (Suc n)  π' (Suc n')
                  using  converged_cd_diverge_cs[OF ip csm ml lnotinπ' lk cseq[symmetric]] .
                have nl: n < l using lcdn is_cdi_def by auto
                hence nk: n<k using lk by auto
                have nretn: π n  return using lcdn by (metis cd_not_ret)
                have nk': n'<k' using cs_order[OF ip csn cseq[symmetric] nretn nk] .
                show ?thesis proof cases
                  assume j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}. vwrites (π' j')
                  thus ?thesis using lcdn csn suc by blast
                next
                  assume ¬(j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}. vwrites (π' j'))
                  then obtain j' where jin': j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'} and vwrite: vwrites (π' j') by blast
                  define i' where i'  LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')
                  have Pk': n' < k'  ( k. cs⇗πk = cs⇗π'k') (is ?P k') using nk' cseq[symmetric] by blast
                  have ni': n' < i' using LeastI[of ?P, OF Pk'] i'_def by auto
                  obtain i where csi: ‹cs⇗πi = cs⇗π'i' using LeastI[of ?P, OF Pk'] i'_def by blast
                  have ij': i'j' using jin'[folded i'_def] by auto
                  have jk': j'<k' using jin'[folded i'_def] by auto
                  have jl': j'  l' using kddl' jk' vwrite unfolding is_ddi_def by auto
                  have nretn': π' n'  return using nretn csn last_cs by metis
                  have iln: n<i using cs_order[OF ip(2,1) csn[symmetric] csi[symmetric] nretn' ni'] .
                  hence mi: m < i using mn by auto
                  have nretm: π m  return by (metis ip(1) mn nretn term_path_stable)
                  have mi': m'<i' using cs_order[OF ip csm csi nretm mi] .
                  have ik': i' < k' using ij' jk' by auto
                  have nreti': π' i'  return by (metis ij' jl' nretl' ip(2) term_path_stable)
                  have ik: i < k using cs_order[OF ip(2,1) csi[symmetric] cseq nreti' ik'] .
                  show ?thesis proof cases
                    assume il:i < l
                    have le: k + k' - (i +i') < k+k' - (m+m') using mi mi' ik ik' by auto
                    show ?thesis using IH[OF le] using csi il by blast
                  next
                    assume ¬ i < l
                    hence li: l  i by auto
                    have i'  l' using ij' jl' by auto
                    hence il': i' < l' using  csi l'notinπ by fastforce 
                    obtain n n' where in': i'  n' and csn: ‹ cs⇗πn = cs⇗π'n' and lcdn': l' cd⇗π'⇖→ n' and suc: π (Suc n)  π' (Suc n')
                      using  converged_cd_diverge_cs[OF ip(2,1) csi[symmetric] il' _ lk' cseq] l'notinπ by metis
                    have nk': n' < k' using lcdn' is_cdi_def lk' by auto
                    have nretn': π' n'  return by (metis cd_not_ret lcdn')
                    have nk: n < k using cs_order[OF ip(2,1) csn[symmetric] cseq nretn' nk'] . 
                    define j where j  LEAST j. n < j  (j'. cs⇗π'j' = cs⇗πj)
                    have Pk: n < k  (j'. cs⇗π'j' = cs⇗πk) (is ?P k) using nk cseq by blast
                    have nj: n<j using LeastI[of ?P, OF Pk] j_def by auto
                    have ilen: i  n using cs_order_le[OF ip(2,1) csi[symmetric] csn[symmetric] nreti' in'] . 
                    hence lj: l<j using li nj by simp
                    have l{l<..<k}. v  writes (π l) using  kddl unfolding is_ddi_def by simp
                    hence nw: l{j..<k}. v  writes (π l) using lj by auto
                    show ?thesis using csn lcdn' suc nw[unfolded j_def] by blast
                  qed
                qed
              next
                assume ml': m' < l'
                obtain n n' where mn': m'  n' and csn: ‹ cs⇗πn = cs⇗π'n' and lcdn': l' cd⇗π'⇖→ n' and suc: π (Suc n)  π' (Suc n')
                  using  converged_cd_diverge_cs[OF ip(2,1) csm[symmetric] ml' _ lk' cseq] l'notinπ by metis
                have nl': n' < l' using lcdn' is_cdi_def by auto
                hence nk': n'<k' using lk' by auto
                have nretn': π' n'  return using lcdn' by (metis cd_not_ret)
                have nk: n<k using cs_order[OF ip(2,1) csn[symmetric] cseq nretn' nk'] .
                show ?thesis proof cases
                  assume j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j)
                  thus ?thesis using lcdn' csn suc by blast
                next
                  assume ¬(j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j))
                  then obtain j where jin: j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k} and vwrite: vwrites (π j) by blast
                  define i where i  LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi)
                  have Pk: n < k  ( k'. cs⇗π'k' = cs⇗πk) (is ?P k) using nk cseq by blast
                  have ni: n < i using LeastI[of ?P, OF Pk] i_def by auto
                  obtain i' where csi: ‹cs⇗πi = cs⇗π'i' using LeastI[of ?P, OF Pk] i_def by metis
                  have ij: ij using jin[folded i_def] by auto
                  have jk: j<k using jin[folded i_def] by auto
                  have jl: j  l using kddl jk vwrite unfolding is_ddi_def by auto
                  have nretn: π n  return using nretn' csn last_cs by metis
                  have iln': n'<i' using cs_order[OF ip csn csi nretn ni] .
                  hence mi': m' < i' using mn' by auto
                  have nretm': π' m'  return by (metis ip(2) mn' nretn' term_path_stable)
                  have mi: m<i using cs_order[OF ip(2,1) csm[symmetric] csi[symmetric] nretm' mi'] .
                  have ik: i < k using ij jk by auto
                  have nreti: π i  return by (metis ij ip(1) jl nret term_path_stable)
                  have ik': i' < k' using cs_order[OF ip csi cseq[symmetric] nreti ik] .
                  show ?thesis proof cases
                    assume il':i' < l'
                    have le: k + k' - (i +i') < k+k' - (m+m') using mi mi' ik ik' by auto
                    show ?thesis using IH[OF le] using csi il' by blast
                  next
                    assume ¬ i' < l'
                    hence li': l'  i' by auto
                    have i  l using ij jl by auto
                    hence il: i < l using  csi lnotinπ' by fastforce 
                    obtain n n' where ilen: i  n and csn: ‹ cs⇗πn = cs⇗π'n' and lcdn: l cd⇗π⇖→ n and suc: π (Suc n)  π' (Suc n')
                      using  converged_cd_diverge_cs[OF ip csi il _ lk cseq[symmetric]] lnotinπ' by metis
                    have nk: n < k using lcdn is_cdi_def lk by auto
                    have nretn: π n  return by (metis cd_not_ret lcdn)
                    have nk': n' < k' using cs_order[OF ip csn cseq[symmetric] nretn nk] . 
                    define j' where j'  LEAST j'. n' < j'  (j. cs⇗πj = cs⇗π'j')
                    have Pk': n' < k'  (j. cs⇗πj = cs⇗π'k') (is ?P k') using nk' cseq[symmetric] by blast
                    have nj': n'<j' using LeastI[of ?P, OF Pk'] j'_def by auto
                    have in': i'  n' using cs_order_le[OF ip csi csn nreti ilen] . 
                    hence lj': l'<j' using li' nj' by simp
                    have l{l'<..<k'}. v  writes (π' l) using  kddl' unfolding is_ddi_def by simp
                    hence nw': l{j'..<k'}. v  writes (π' l) using lj' by auto
                    show ?thesis using csn lcdn suc nw'[unfolded j'_def] by blast
                  qed
                qed
              qed
            qed
            then obtain n n' where csn: ‹ cs⇗πn = cs⇗π'n' and suc: π (Suc n)  π' (Suc n')
            and cdor: 
            (l cd⇗π⇖→ n  (j'{(LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i'))..<k'}. vwrites (π' j'))
             l' cd⇗π'⇖→ n'  (j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j))) 
            by blast
            show ?thesis using cdor proof
              assume *: l cd⇗π⇖→ n  (j'{LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')..<k'}. v  local.writes (π' j'))
              hence lcdn: l cd⇗π⇖→ n by blast 
              have nowrite: j'{LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')..<k'}. v  local.writes (π' j') using * by blast
              show ?thesis proof (rule cp.intros(3)[of σ n σ' n',folded path])
                show l cd⇗π⇖→ n using lcdn .
                show k dd⇗π,v⇖→ l using kddl .
                show ‹cs⇗πk = cs⇗π'k' using cseq by simp
                show π (Suc n)  π' (Suc n') using suc by simp
                show j'{LEAST i'. n' < i'  (i. cs⇗πi = cs⇗π'i')..<k'}. v  local.writes (π' j') using nowrite .
                show (σk) v  (σ'k') v using vneq .
                have nk: n < k using lcdn lk is_cdi_def by auto
                have nretn: π n  return using cd_not_ret lcdn by metis
                have nk': n' < k' using cs_order[OF ip csn cseq[symmetric] nretn nk] .
                hence le: n + n' < k + k' using nk by auto
                moreover
                have 1: π (Suc n) = suc (π n) (σn) by (metis step_suc_sem fst_conv path(1) path_suc)
                have 2: π' (Suc n') = suc (π' n') (σ'n') by (metis step_suc_sem fst_conv path(2) path_suc)
                have 3: π' n' = π n using csn last_cs by metis
                have nreads: σn reads (π n)  σ'n' reads (π n) by (metis 1 2 3 suc reads_restr_suc)
                then obtain v' where v'read: v'reads (path σ n) (σn) v'  (σ'n') v' by (metis path(1) reads_restrict)
                ultimately  
                show ((σ, n), (σ', n'))  cp using IH csn path by auto
              qed
            next
              assume *: l' cd⇗π'⇖→ n'  (j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j))
              hence lcdn': l' cd⇗π'⇖→ n' by blast 
              have nowrite: j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j) using * by blast
              show ?thesis proof (rule cp.intros(4), rule cp.intros(3)[of σ' n' σ n,folded path])
                show l' cd⇗π'⇖→ n' using lcdn' .
                show k' dd⇗π',v⇖→ l' using kddl' .
                show ‹cs⇗π'k' = cs⇗πk using cseq .
                show π' (Suc n')  π (Suc n) using suc by simp
                show j{(LEAST i. n < i  (i'. cs⇗π'i' = cs⇗πi))..<k}. vwrites (π j) using nowrite .
                show (σ'k') v  (σk) v using vneq by simp
                have nk': n' < k' using lcdn' lk' is_cdi_def by auto
                have nretn': π' n'  return using cd_not_ret lcdn' by metis
                have nk: n < k using cs_order[OF ip(2,1) csn[symmetric] cseq nretn' nk'] .
                hence le: n + n' < k + k' using nk' by auto
                moreover
                have 1: π (Suc n) = suc (π n) (σn) by (metis step_suc_sem fst_conv path(1) path_suc)
                have 2: π' (Suc n') = suc (π' n') (σ'n') by (metis step_suc_sem fst_conv path(2) path_suc)
                have 3: π' n' = π n using csn last_cs by metis
                have nreads: σn reads (π n)  σ'n' reads (π n) by (metis 1 2 3 suc reads_restr_suc)
                then obtain v' where v'read: v'reads (path σ n) (σn) v'  (σ'n') v' by (metis path(1) reads_restrict)
                ultimately  
                have ((σ, n), (σ', n'))  cp using IH csn path by auto
                thus ((σ', n'), σ, n)  cp using cp.intros(4) by simp                
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed


theorem contradicting_in_cop: assumes σ =L σ' and (σ',k') 𝔠 (σ,k) and path σ k  dom att 
shows ((σ,k),σ',k')  cop using assms(2) proof(cases) 
  case (1 π' π) 
  define j where j  π ¡ cs⇗π'k'
  have csj: ‹cs⇗πj = cs⇗π'k' unfolding j_def using 1 by (metis cs_not_nil cs_select_is_cs(1) path_is_path)
  have suc: π (Suc j)  π' (Suc k') using 1 j_def by simp
  have kcdj: k cd⇗π⇖→ j by (metis cs_not_nil cs_select_is_cs(2) 1(1,2) j_def path_is_path)
  obtain v where readv: vreads(path σ j) and vneq: (σj) v  (σ'k') v using suc csj unfolding 1 by (metis IFC_def.suc_def 1(2) 1(3) last_cs path_suc reads_restr_suc reads_restrict)
  have ((σ,j),σ',k')  cp apply (rule contradicting_in_cp[OF assms(1)]) using readv vneq csj 1 by auto
  thus ((σ,k),σ',k')  cop using kcdj suc assms(3) cop.intros(2) unfolding 1 by auto
  next
  case (2 π' π)
  obtain v where readv: vreads(path σ k) and vneq: (σk) v  (σ'k') v using 2(2-4) by (metis reads_restrict)
  have ((σ,k),σ',k')  cp apply (rule contradicting_in_cp[OF assms(1)]) using readv vneq 2 by auto
  thus ((σ,k),σ',k')  cop using assms(3) cop.intros(1) unfolding 2 by auto
qed


theorem cop_correct_term: fixes σ σ' defines π: π  path σ and π': π'  path σ' 
assumes ret: π n = return π' n' = return and obsne: obs σ  obs σ' and leq: σ =L σ'
shows  k k'. ((σ,k),σ',k') cop  ((σ',k'),σ,k) cop
proof -
  have *:  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom (att))  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom (att)) using  obs_neq_contradicts_term ret obsne π π' by auto
  have leq' :σ' =L σ using leq unfolding loweq_def by auto
  from * contradicting_in_cop[OF leq] contradicting_in_cop[OF leq'] show ?thesis unfolding π π' by metis
qed


theorem cop_correct_ret: fixes σ σ' defines π: π  path σ and π': π'  path σ' 
assumes ret: π n = return and obsne: obs σ i  obs σ' i and obs: obs σ' i  None and leq: σ =L σ'
shows  k k'. ((σ,k),σ',k') cop  ((σ',k'),σ,k) cop
proof -
  have *:  k k'. ((σ', k') 𝔠 (σ ,k)  π k  dom (att))  ((σ, k) 𝔠 (σ' ,k')  π' k'  dom (att))
    by (metis (no_types, lifting) π π' obs obs_neq_ret_contradicts obsne ret) 
  have leq' :σ' =L σ using leq unfolding loweq_def by auto
  from * contradicting_in_cop[OF leq] contradicting_in_cop[OF leq'] show ?thesis unfolding π π' by metis
qed


theorem cop_correct_nterm: assumes obsne: obs σ k  obs σ' k obs σ k  None obs σ' k  None 
and leq: σ =L σ'
shows  k k'. ((σ,k),σ',k') cop  ((σ',k'),σ,k) cop
proof -
  obtain k k' where ((σ', k') 𝔠 (σ ,k)  path σ k  dom att)  ((σ, k) 𝔠 (σ' ,k')  path σ' k'  dom att) 
  using obs_neq_some_contradicts[OF obsne] by metis
  thus ?thesis proof
    assume *: (σ', k') 𝔠 (σ ,k)  path σ k  dom att
    hence ((σ,k),σ',k')  cop using leq by (metis contradicting_in_cop)
    thus ?thesis using * by blast
  next 
    assume *: (σ, k) 𝔠 (σ' ,k')  path σ' k'  dom att
    hence ((σ',k'),σ,k)  cop using leq by (metis contradicting_in_cop loweq_def)
    thus ?thesis using * by blast
  qed
qed


subsection ‹Correctness of the Characterisation›
text_raw ‹\label{sec:cor-cp}›

text ‹The following is our main correctness result. If there exist no critical observable paths,
then the program is secure.›

theorem cop_correct: assumes cop = empty shows secure proof (rule ccontr)
  assume ¬ secure
  then obtain σ σ' where leq: σ =L σ' 
    and **: ¬ obs σ  obs σ'  (terminates σ  ¬ obs σ'  obs σ)
    unfolding secure_def by blast
  show False using ** proof
    assume ¬ obs σ  obs σ'
    then obtain k where obs σ k  obs σ' k  obs σ k  None  obs σ' k  None 
      unfolding obs_comp_def obs_prefix_def
      by (metis kth_obs_stable linorder_neqE_nat obs_none_no_kth_obs obs_some_kth_obs) 
    thus False using cop_correct_nterm leq assms by auto
  next
    assume *: terminates σ  ¬ obs σ'  obs σ
    then obtain n where ret: path σ n = return  
      unfolding terminates_def by auto
    obtain k where obs σ k  obs σ' k  obs σ' k  None using * unfolding obs_prefix_def by metis 
    thus False using cop_correct_ret ret leq assms by (metis empty_iff) 
  qed
qed


text ‹Our characterisation is not only correct, it is also precise in the way that cp› characterises 
exactly the matching indices in executions for low equivalent input states where diverging data is read. 
This follows easily as the inverse implication to lemma contradicting_in_cp› can be shown by simple induction.›

theorem cp_iff_reads_contradict: ((σ,k),(σ',k'))  cp  σ =L σ'  cs⇗path σk = cs⇗path σ'k'  ( vreads(path σ k). (σk) v  (σ'k') v) 
proof
  assume σ =L σ'  cs⇗path σk = cs⇗path σ'k'  (vreads (path σ k). (σk) v  (σ'k') v)
  thus ((σ, k), σ', k')  cp using contradicting_in_cp by blast 
next
  assume ((σ, k), σ', k')  cp 
  thus σ =L σ'  cs⇗path σk = cs⇗path σ'k'  (vreads (path σ k). (σk) v  (σ'k') v)
  proof (induction)
    case (1 σ σ' n n' h)
    then show ?case by blast 
  next
    case (2 σ k σ' k' n v n')
    have vreads (path σ n) using 2(2) unfolding is_ddi_def by auto
    then show ?case using 2 by auto
  next
    case (3 σ k σ' k' n v l n')
    have vreads (path σ n) using 3(2) unfolding is_ddi_def by auto
    then show ?case using 3(4,6,8) by auto
  next
    case (4 σ k σ' k')
    hence ‹cs⇗path σk = cs⇗path σ'k' by simp
    hence path σ' k' = path σ k by (metis last_cs) 
    moreover have σ' =L σ using 4(2) unfolding loweq_def by simp
    ultimately show ?case using 4 by metis
  qed
qed


text ‹In the same way the inverse implication to contradicting_in_cop› follows easily 
such that we obtain the following characterisation of cop›.›

theorem cop_iff_contradicting: ((σ,k),(σ',k'))  cop  σ =L σ'  (σ',k') 𝔠 (σ,k)  path σ k  dom att 
proof
  assume σ =L σ'  (σ', k') 𝔠 (σ, k)  path σ k  dom att thus ((σ,k),(σ',k'))  cop using contradicting_in_cop by simp
next
  assume ((σ,k),(σ',k'))  cop 
  thus σ =L σ'  (σ',k') 𝔠 (σ,k)  path σ k  dom att proof (cases rule: cop.cases)
    case 1
    then show ?thesis using cp_iff_reads_contradict contradicts.simps by (metis (full_types) reads_restrict1)
  next
    case (2 k)
    then show ?thesis using cp_iff_reads_contradict contradicts.simps
      by (metis cd_is_cs_less cd_not_ret contradicts.intros(1) cs_select_id path_is_path) 
  qed
qed


subsection ‹Correctness of the Single Path Approximation›
text_raw ‹\label{sec:cor-scp}›

theorem cp_in_scp: assumes ((σ,k),(σ',k'))cp shows (path σ,k)scp  (path σ',k')scp 
using assms proof(induction σ k σ' k' rule:cp.induct[case_names read_high dd dcd sym])
  case (read_high σ σ' k k' h) 
  have σ h = (σk) h using read_high(5) by (simp add: no_writes_unchanged0)
  moreover have σ' h = (σ'k') h using read_high(6) by (simp add: no_writes_unchanged0)
  ultimately have σ h  σ' h using read_high(4) by simp 
  hence *: hhvars using read_high(1) unfolding loweq_def by (metis Compl_iff IFC_def.restrict_def)
  have 1: (path σ,k)scp using scp.intros(1) read_high(3,5) * by auto
  have path σ k = path σ' k' using read_high(2) by (metis last_cs)
  hence (path σ',k')scp using scp.intros(1) read_high(3,6) * by auto
  thus ?case using 1 by auto
next
  case dd show ?case using scp.intros(3) dd by auto  
next 
  case sym thus ?case by blast
next
  case (dcd σ k σ' k' n v l n')   
  note scp.intros(4) is_dcdi_via_def cd_cs_swap cs_ipd
  have 1: (path σ, n)scp using dcd.IH dcd.hyps(2) dcd.hyps(3) scp.intros(2) scp.intros(3) by blast 
  have csk: ‹cs⇗path σk = cs⇗path σ'k' using cp_eq_cs[OF dcd(1)] .
  have kn: k<n and kl: k<l and ln: l<n using dcd(2,3) unfolding is_ddi_def is_cdi_def by auto
  have nret: path σ k  return using cd_not_ret dcd.hyps(3) by auto
  have k' < n' using kn csk dcd(4) cs_order nret path_is_path last_cs by blast
  have 2: (path σ', n')scp proof cases    
    assume j'ex: j'{k'..<n'}. v  writes (path σ' j')
    hence j'. j'{k'..<n'}  v  writes (path σ' j') by auto
    note * = GreatestI_ex_nat[OF this]
    define j' where j' == GREATEST j'. j'{k'..<n'}  v  writes (path σ' j')
    note ** = *[of j',folded j'_def]  
    have k'  j' j'<n' and j'write: v  writes (path σ' j')
      using "*" atLeastLessThan_iff j'_def nat_less_le by auto
    have nowrite:  i'{j'<..<n'}. v  writes(path σ' i') proof (rule, rule ccontr)
      fix i' assume i'  {j'<..<n'} ¬ v  local.writes (path σ' i')
      hence i'  {k'..<n'}  v  local.writes (path σ' i') using k'  j' by auto
      hence i'  j' using Greatest_le_nat
        by (metis (no_types, lifting) atLeastLessThan_iff j'_def nat_less_le)
      thus False using i'  {j'<..<n'} by auto
    qed
    have path σ' n' = path σ n using dcd(4) last_cs by metis
    hence vreads(path σ' n') using dcd(2) unfolding is_ddi_def by auto    
    hence nddj': n' dd⇗path σ',v⇖→ j' using dcd(2) unfolding is_ddi_def using nowrite j'<n' j'write by auto 
    show ?thesis proof cases
      assume j' cd⇗path σ'⇖→ k'
      thus (path σ',n')  scp using scp.intros(2) scp.intros(3) dcd.IH nddj' by fast
    next
      assume jcdk': ¬ j' cd⇗path σ'⇖→ k'
      show ?thesis proof cases
        assume j' = k'
        thus ?thesis using scp.intros(3) dcd.IH nddj' by fastforce 
      next
        assume j'  k' hence k' < j' using k'  j' by auto
        have path σ' j'  return using j'write writes_return by auto
        hence ipdex':j. j {k'..j'}  path σ' j = ipd (path σ' k') using path_is_path k' < j' jcdk' is_cdi_def by blast
        define i' where i' == LEAST j. j {k'..j'}  path σ' j = ipd (path σ' k')        
        have iipd': i' {k'..j'} path σ' i' = ipd (path σ' k') unfolding i'_def using LeastI_ex[OF ipdex'] by simp_all
        have *: i  {k'..<i'}. path σ' i  ipd (path σ' k') proof (rule, rule ccontr)
          fix i assume  *: i  {k'..<i'} ¬ path σ' i  ipd (path σ' k')
          hence **: i {k'..j'}  path σ' i = ipd (path σ' k') (is ?P i) using iipd'(1) by auto
          thus False using Least_le[of ?P i] i'_def * by auto
        qed
        have i'  k' using iipd'(2) by (metis csk last_cs nret path_in_nodes ipd_not_self)
        hence k'<i' using iipd'(1) by simp
        hence csi': ‹cs⇗path σ'i' = [ncs⇗path σ'k' . ipd n  path σ' i'] @ [path σ' i']using cs_ipd[OF iipd'(2) *] by fast 
        
        have ncdk': ¬ n' cd⇗path σ'⇖→ k' using j' < n' k' < j' cdi_prefix jcdk' less_imp_le_nat by blast
        hence ncdk: ¬ n cd⇗path σ⇖→ k using cd_cs_swap csk dcd(4) by blast        
        have ipdex: i. i{k..n}  path σ i = ipd (path σ k) (is i. ?P i) proof cases
          assume *:path σ n = return 
          from path_ret_ipd[of path σ k n,OF path_is_path nret *]          
          obtain i where ?P i by fastforce thus ?thesis by auto
        next
          assume *:path σ n  return           
          show ?thesis using not_cd_impl_ipd [of path σ k n, OF path_is_path k<n ncdk *] by auto
        qed
        
        define i where  i == LEAST j. j {k..n}  path σ j = ipd (path σ k)        
        have iipd: i {k..n} path σ i = ipd (path σ k) unfolding i_def using LeastI_ex[OF ipdex] by simp_all
        have **: i'  {k..<i}. path σ i'  ipd (path σ k) proof (rule, rule ccontr)
          fix i' assume  *: i'  {k..<i} ¬ path σ i'  ipd (path σ k)
          hence **: i' {k..n}  path σ i' = ipd (path σ k) (is ?P i') using iipd(1) by auto
          thus False using Least_le[of ?P i'] i_def * by auto
        qed
        have i  k using iipd(2) by (metis nret path_in_nodes ipd_not_self)
        hence k<i using iipd(1) by simp
        hence ‹cs⇗path σi = [ncs⇗path σk . ipd n  path σ i] @ [path σ i]using cs_ipd[OF iipd(2) **] by fast 
        hence csi: ‹cs⇗path σi = cs⇗path σ'i' using csi' csk unfolding iipd'(2) iipd(2) by (metis last_cs)
        hence (LEAST i'. k' < i'  (i. cs⇗path σi = cs⇗path σ'i'))  i' (is (LEAST x. ?P x)  _) 
          using k' < i' Least_le[of ?P i'] by blast
        hence nw: j'{i'..<n'}. v  writes (path σ' j') using dcd(7) allB_atLeastLessThan_lower by blast  
        moreover have v  writes (path σ' j') using nddj' unfolding is_ddi_def by auto
        moreover have i'  j' using iipd'(1) by auto
        ultimately have False  using j' < n' by auto
        thus ?thesis ..
      qed
    qed
  next
    assume ¬ (j'{k'..<n'}. v  writes (path σ' j'))
    
    hence n' dcd⇗path σ',v⇖→ k' via (path σ) k unfolding is_dcdi_via_def using dcd(2-4) csk k'<n' path_is_path by metis    
    thus ?thesis using dcd.IH scp.intros(4) by blast 
  qed
  with 1 show ?case ..
qed   


theorem cop_in_scop: assumes ((σ,k),(σ',k'))cop shows (path σ,k)scop  (path σ',k')scp
  using assms 
  apply (induct rule: cop.induct)
   apply (simp add: cp_in_scp)
  using cp_in_scp scop.intros scp.intros(2)
   apply blast
  using cp_in_scp scop.intros scp.intros(2)
  apply blast
  done

text ‹The main correctness result for out single execution approximation follows directly.›

theorem scop_correct: assumes scop = empty shows secure 
  using cop_correct assms cop_in_scop by fast 

end

end