Theory SLA_Criterion

(*Certified Infinite Descent Criteria in Isabelle/HOL *)
(*Authors: Jamie Wright, Liron Cohen, Reuben Rowe and Andrei Popescu*)

subsubsection "Slope-language Criterion"
theory SLA_Criterion
  imports "../Sloped_Graphs"
          "../Buchi_Preliminaries"
begin

context Sloped_Graph 
begin

abbreviation q⇩₀ where "q⇩₀ ≡ None"
fun RR':: "'node × 'node ⇒ 'pos × 'pos × slope ⇒ bool"  where "RR' (nd,nd') = (λ(ps, ps', s). RR (nd,ps) (nd',ps') s)"


fun ndOf where "ndOf ((nd,ps),(nd',ps'),s) = nd"
fun nd'Of where "nd'Of ((nd,ps),(nd',ps'),s) = nd'"

term "{Some nd'| nd. edge nd nd'}"
(*PATH AUTOMATON*)
fun Δ⇩_s⇩_l :: "('pos × 'pos × slope ⇒ bool) ⇒ 'node option ⇒ 'node option set" where
  "Δ⇩_s⇩_l t (Some nd) = {Some nd'| nd'. {nd, nd'} ⊆ Node ∧ edge nd nd' ∧ t = RR'(nd,nd') }"|
  "Δ⇩_s⇩_l t q⇩₀ = {Some nd'| nd nd'. {nd, nd'} ⊆ Node ∧ edge nd nd' ∧ t = RR'(nd,nd')}"

lemma Δ⇩_s⇩_l_intro_Some:
  assumes "edge s s'" 
    and "{s, s'} ⊆ Node"
    and "tr = RR'(s,s')"
  shows "Some s' ∈ Δ⇩_s⇩_l tr (Some s)"
  using assms by auto

lemma Δ⇩_s⇩_l_intro_q0:
  assumes  "edge s s'" 
    and "{s, s'} ⊆ Node"
    and "tr = RR'(s,s')"
  shows "Some s' ∈ Δ⇩_s⇩_l tr q⇩₀"
  using assms by auto

lemma Δ⇩_s⇩_l_elim:
  assumes "x ∈ Δ⇩_s⇩_l t z"
  obtains nd nd' where
    "x = Some nd'" "nd ∈ Node" "nd' ∈ Node" "edge nd nd'" "t = RR' (nd, nd')"
    "z = q⇩₀ ∨ the z = nd"
  using assms by (cases z, auto)

lemma Δ⇩_s⇩_l_q⇩₀_not_q⇩₀[simp]: "¬ (q⇩₀ ∈ Δ⇩_s⇩_l x q⇩₀)" by auto

lemma Δ⇩_s⇩_l_some:"r' ∈ Δ⇩_s⇩_l x r ⟹ ∃y. r' = Some y" by(cases r, auto) 

(*Sanity check with the Δ⇩_s⇩_l in the paper, 
  the sets of transitions as before*)
lemma "Δ⇩_s⇩_l l s = 
       {Some v'| v v'. s = q⇩₀ ∧ (edge v v') ∧ {v, v'} ⊆ Node ∧ l = RR'(v,v')} ∪
       {Some v'| v'. s ≠ q⇩₀ ∧ edge (the s) v' ∧ {(the s), v'} ⊆ Node ∧ l = RR'((the s),v')}"
  unfolding Δ⇩_s⇩_l.simps by(cases s, auto)

definition Paut⇩_R :: "('pos × 'pos × slope ⇒ bool, 'node option) nba" where
  "Paut⇩_R = nba 
    {RR' (nd, nd')| nd nd'. edge nd nd'}
    {q⇩₀}
    Δ⇩_s⇩_l
    (λs. the s ∈ Node)"

lemmas Paut⇩_R_defs = Paut⇩_R_def Δ⇩_s⇩_l.simps
lemma Paut⇩_R_alpha[simp]:"nba.alphabet Paut⇩_R = {RR' (nd, nd')| nd nd'. edge nd nd'}" unfolding Paut⇩_R_def by auto
lemma Paut⇩_R_accept[simp]:"nba.accepting Paut⇩_R = (λs. the s ∈ Node)" unfolding Paut⇩_R_def by auto
lemma Paut⇩_R_init[simp]: "nba.initial Paut⇩_R = {q⇩₀}" unfolding Paut⇩_R_def by auto
lemma Paut⇩_R_initp[intro]:"p ∈ nba.initial Paut⇩_R ⟷ p = q⇩₀" by auto
lemma Paut⇩_R_trans[simp]:"nba.transition Paut⇩_R a b = Δ⇩_s⇩_l a b" unfolding Paut⇩_R_def by auto

lemmas Paut⇩_R_trans' = Paut⇩_R_trans Δ⇩_s⇩_l.simps
lemmas Paut⇩_R_run_def = nba.run_alt_def_snth Paut⇩_R_trans Paut⇩_R_alpha nba.target_alt_def  nba.states_alt_def


lemma Paut⇩_R_lang:"NBA.language Paut⇩_R = {Ri. ∃nds. ipath nds ∧ (∀i. Ri !! i = RR' (nds !! i, nds !! Suc i))}" 
proof(safe)
  fix x 
  assume "x ∈ NBA.language Paut⇩_R"
  then obtain r where run:"NBA.run Paut⇩_R (x ||| r) None"  and accept:"infs (λs. the s ∈ Node) r" apply-by(erule nba.language_elim, auto)


  (*We leave q⇩₀ immediately and never transition back during the run*)
  have q⇩₀'_notReachable:"⋀k. r !! k ≠ q⇩₀"
      subgoal for k apply(induct k)
        subgoal using runE_0[OF run] apply-by(clarsimp)
        subgoal for k using runE_Suc[OF run, of k] by auto . .

  have x_prop:"⋀k. k>0 ⟹ ∃nd nd'. x !! k = RR' (nd, nd') ∧ edge nd nd' ∧ the(r!!k) = nd'  ∧ the(r!!(k-1)) = nd" 
    subgoal for k  
      using runE_Suc[OF run, of k, unfolded Paut⇩_R_trans]
      apply-apply(drule runE_Suc'[OF run, of k, unfolded Paut⇩_R_trans])
      apply(erule Δ⇩_s⇩_l_elim)+
      using q⇩₀'_notReachable[of] by auto . 


  have q⇩₀'_notLast:"⋀k. k>0 ⟹ last (stake k r) ≠ q⇩₀" subgoal for k
     using q⇩₀'_notReachable[of "k-1"] last_conv_nth[of "stake k r"] by auto .
  
  hence i_eq_iff:"⋀i. (if i = 0 then None else last (stake i r)) = None ⟷ i = 0" by simp

  obtain s where s_edge:"edge s (the (r !! 0))" and s_node:"s ∈Node" and s_x:"x !! 0 = RR'(s, the (r !! 0))"
    using runE_0[OF run] by auto

  show "∃nds. local.ipath nds ∧ (∀i. x !! i = RR' (nds !! i, nds !! Suc i))"
  proof(rule exI[of _ "s ## smap the r"], unfold ipath_def Paut⇩_R_initp Paut⇩_R_accept, safe)
    fix i

    have "alw (holdsS Node) (smap the r)" unfolding alw_holdsS_iff_snth apply-apply(rule allI)
      subgoal for i apply(induct i)
        subgoal using runE_0[OF run] by auto 
        subgoal for i using runE_Suc[OF run, of i, unfolded Paut⇩_R_trans] apply-by(erule Δ⇩_s⇩_l_elim, auto) . . 

    thus "alw (holdsS Node) (s ## smap the r)"
      using s_node unfolding alw_holdsS_iff_snth by (metis not0_implies_Suc snth.simps(1) snth_Stream stream.sel(1))

 

    have alwEdge:"alw (holds2 edge) (smap the r)" unfolding alw_holds2_iff_snth apply-apply(rule allI)
      subgoal for i using runE_Suc[OF run, of i, unfolded Paut⇩_R_trans] 
                          runE_Suc[OF run, of "Suc i", unfolded Paut⇩_R_trans]
          apply-apply(erule Δ⇩_s⇩_l_elim)+
          using q⇩₀'_notReachable by auto .
          
    thus "alw (holds2 edge) (s ## smap the r)"
      using s_edge unfolding alw_holds2_iff_snth apply-apply(rule allI)
      subgoal for i apply(cases i, simp)
        subgoal for n by (erule allE[of _ n], auto) . . 

    show "x !! i = RR' ((s ## smap the r) !! i, (s ## smap the r) !! Suc i)" 
      using s_x x_prop[of i] by(cases i, auto)
  qed
next
  fix x nds
  assume ipath:"ipath nds" and
         Rel:"∀i. x !! i = RR' (nds !! i, nds !! Suc i)"
  obtain nd1 nd2 where nds:"nds = nd1 ## nd2" by (cases nds)
  have Rel':"⋀i. x !! i = RR' (nds !! i, nds !! Suc i) ∧ edge (nds !! i) (nds !! Suc i)" 
    using Rel RR'.simps ipath unfolding alw_holds2_iff_snth ipath_def by auto

  have nds_in_Node:"sset nds ⊆ Node" by (metis ipath sset_ipath)
  hence stl_nds_in_Node:"sset (stl nds) ⊆ Node" using nds by auto

  show "x ∈ NBA.language Paut⇩_R"
  proof(rule nba.language[of None Paut⇩_R x "smap Some (stl nds)"])

    show "q⇩₀ ∈ nba.initial Paut⇩_R" by auto

    show "NBA.run Paut⇩_R (x ||| smap Some (stl nds)) q⇩₀"
    proof(unfold Paut⇩_R_run_def fst_nth_zip snd_nth_zip, intro allI conjI, safe)
      fix k
      show " ∃nd nd'. x !! k = RR' (nd, nd') ∧ edge nd nd'" using Rel' by auto
      show "smap Some (stl nds) !! k ∈ Δ⇩_s⇩_l (x !! k) (last (None # map snd (stake k (x ||| smap Some (stl nds)))))"
      proof(induct k)
        case 0
        have last:"(last (None # map snd (stake 0 (x ||| smap Some (stl nds))))) = None" by auto
        show ?case unfolding snth_smap last
          apply(rule Δ⇩_s⇩_l_intro_q0[of "shd nds" ])
          subgoal using Rel'[of 0] by auto
          subgoal using nds_in_Node stl_nds_in_Node by auto
          subgoal using Rel'[of 0] by auto .
     next
        case (Suc k)
        then show ?case unfolding last_stake_szip snth_smap
          apply-apply(erule Δ⇩_s⇩_l_elim,rule Δ⇩_s⇩_l_intro_Some) 
          using Rel'[of "Suc k"]  ipath ipath_iff_snth ipath_stl nds_in_Node by auto
      qed
    qed


    have ruleInfs:"infs (nba.accepting Paut⇩_R) (smap Some (stl nds)) ⟹infs (nba.accepting Paut⇩_R) (q⇩₀ ## smap Some (stl nds))"
      using alw_ev_shift[of _ "[None]"] by auto

    show "infs (nba.accepting Paut⇩_R) (q⇩₀ ## smap Some (stl nds))"
      apply(rule ruleInfs,rule infs_all)
      using stl_nds_in_Node by auto
  qed
qed

lemma Paut⇩_R_lang_in:"x ∈ NBA.language Paut⇩_R ⟷ (∃nds. ipath nds ∧ (∀i. x !! i = RR' (nds !! i, nds !! Suc i)))"
  unfolding Paut⇩_R_lang by auto



(*What the states should be, per the paper:*)
definition Q'⇩_s⇩_l::"('pos × slope) set" where 
"Q'⇩_s⇩_l ≡ {(p, s)| p s. p ∈ (⋃v∈Node. PosOf v)}"
abbreviation "Σ ≡ {RR' (nd, nd')| nd nd'. edge nd nd'}"
(*TRACE AUTO*)
fun Δ⇩_s⇩_l' :: "('pos × 'pos × slope ⇒ bool) ⇒ ('pos × slope) option ⇒ ('pos × slope) option set" where
  "Δ⇩_s⇩_l' R' (Some (p,s)) = {Some (p',s')| p' s'. (p,s) ∈ Q'⇩_s⇩_l ∧ R' ∈ Σ ∧ R' (p, p', s')}"|
  "Δ⇩_s⇩_l' R' q⇩₀ = (if R' ∈ Σ then {q⇩₀} ∪ {Some (p',s')| p' s'. (p',s') ∈ Q'⇩_s⇩_l} else {})"

(*intros*)
lemma Δ⇩_s⇩_l'_intro_Some:
  assumes "(p, s) ∈ Q'⇩_s⇩_l" "R' ∈ Σ" "R' (p, p', s')"
  shows "Some (p', s') ∈ Δ⇩_s⇩_l' R' (Some (p, s))"
  using assms by auto

lemma Δ⇩_s⇩_l'_intro_q0:
  assumes "R' ∈ Σ" "(p', s') ∈ Q'⇩_s⇩_l"
  shows "Some (p', s') ∈ Δ⇩_s⇩_l' R' q⇩₀"
  using assms by auto

lemma Δ⇩_s⇩_l'_q0_included:
  assumes "R' ∈ Σ"
  shows "q⇩₀ ∈ Δ⇩_s⇩_l' R' q⇩₀"
  using assms by auto

lemma Δ⇩_s⇩_l'_intro:
  assumes "ns ∈ Σ"
  assumes "rk ≠ q⇩₀ ⟹ (∃ p' s'. rk' = Some (p', s') ∧ the rk ∈ Q'⇩_s⇩_l ∧ ns (fst(the rk), p', s'))"
  assumes "rk = q⇩₀ ⟹ (rk' = q⇩₀ ∨ (∃p' s'. rk' = Some (p', s') ∧ (p', s') ∈ Q'⇩_s⇩_l))"
  shows "rk' ∈ Δ⇩_s⇩_l' ns rk"
  using assms apply (cases rk) by force+



(*elims*)
lemma Δ⇩_s⇩_l'_elim:
  assumes "x ∈ Δ⇩_s⇩_l' R' z"
  obtains (SomeCase) p s p' s' where 
    "z = Some (p, s)" "x = Some (p', s')" "(p, s) ∈ Q'⇩_s⇩_l" "R' ∈ Σ" "R' (p, p', s')"
  | (q0Case) p' s' where 
    "z = q⇩₀" "R' ∈ Σ" "(p', s') ∈ Q'⇩_s⇩_l" "x = Some (p', s')"
  | (q0Self) "z = q⇩₀" "R' ∈ Σ" "x = q⇩₀"
  using assms by (cases z,(auto split: if_splits)+)

(*If we transition from a state which is not q⇩₀, then we can never return*)
lemma q⇩₀_notReachable:"q ≠ q⇩₀ ⟹ v' ∈ Δ⇩_s⇩_l' v q ⟹ v' ≠ q⇩₀" by(cases v', cases q, auto)





definition F⇩_s⇩_l::"('pos × slope) option ⇒ bool" where 
"F⇩_s⇩_l ≡ λps. ∃p. ps = Some (p, Decr) ∧ (p, Decr) ∈ Q'⇩_s⇩_l"


definition Taut⇩_R :: "('pos × 'pos × slope ⇒ bool, ('pos × slope) option) nba" where
  "Taut⇩_R = nba 
    {RR' (nd, nd')| nd nd'. edge nd nd'}
    {q⇩₀}
    Δ⇩_s⇩_l'
    F⇩_s⇩_l"

lemma RR_reduce:"(∀n≥Suc 0. RR (r1 !! n, Ps !! n) (stl r1 !! n, stl Ps !! n) (stl Ss !! n)) ⟷
       (∀n. RR (stl r1 !! n, stl Ps !! n) (stl(stl r1) !! n, stl(stl Ps) !! n) (stl(stl Ss) !! n))"
  apply standard
subgoal by auto
  subgoal apply(rule allI)
    subgoal for n by(cases n, auto) . .


(*lemma kk:"⋀k. k>0 ⟹ r !! (k - Suc 0) = last (stake k r)" subgoal for k using last_conv_nth[of "stake k r"] by auto .
*)

lemma Taut⇩_R_alpha[simp]:"nba.alphabet Taut⇩_R = {RR' (nd, nd')| nd nd'. edge nd nd'}" unfolding Taut⇩_R_def by auto
lemma Taut⇩_R_accept[simp]:"nba.accepting Taut⇩_R = (λps. ∃p. ps = Some (p, Decr) ∧ (p, Decr) ∈ Q'⇩_s⇩_l)" unfolding Taut⇩_R_def F⇩_s⇩_l_def by auto
lemma Taut⇩_R_init[simp]: "nba.initial Taut⇩_R = {q⇩₀}" unfolding Taut⇩_R_def by auto
lemma Taut⇩_R_initp[intro]:"p ∈ nba.initial Taut⇩_R ⟷ p = q⇩₀" by auto
lemma Taut⇩_R_trans[simp]:"nba.transition Taut⇩_R a b = Δ⇩_s⇩_l' a b" unfolding Taut⇩_R_def by auto

lemmas run_def' = nba.run_alt_def_snth fst_nth_zip snd_nth_zip Taut⇩_R_trans Taut⇩_R_alpha nba.target_alt_def  nba.states_alt_def


(**converting a stream of nodes to it's Ri sequence**)
fun Rst where "Rst nds = smap (λi. RR' (nds !! i, nds !! Suc i)) nats"

lemma stl_shift:"(stl nds !! i,stl (stl nds) !! i) = (nds !! Suc i,(stl nds) !! Suc i)" by auto

lemma smap_shifted_eq:
        "smap (λi. RR' (nds !! i,stl nds !! i)) (fromN (Suc 0)) = 
         smap (λi. RR' (stl nds !! i,stl (stl nds) !! i)) nats"
  unfolding stl_shift
  apply(rule ssubst[of "smap (λi. RR' (nds !! Suc i, stl nds !! Suc i)) nats" 
                       "smap (λj (ps, ps', y). RR (stl nds !! (j - Suc 0), ps) (stl (stl nds) !! (j - Suc 0), ps') y) (fromN (Suc 0))"])
  subgoal using stream_smap_fromN[of "smap (λi. RR' (stl nds !! i, stl (stl nds) !! i)) nats" "Suc 0"] by auto
  apply(rule stream.map_cong0)
  subgoal for z using stl_Suc[of z nds] stl_Suc[of "z" "stl nds"] by force .

lemma Rst_correct:"x = Rst nds ⟷ (∀i. x !! i = RR' (nds !! i, nds !! Suc i))"
  apply(safe)
  subgoal for i by(cases i, auto)
  subgoal 
    apply (coinduction arbitrary: x nds, intro conjI)
    subgoal by (erule allE[of _ 0], auto)
    subgoal for x_hd x_tl nd_hd nd_tl x nds 
      apply(rule exI2[of _ x_tl "stl nds"], safe)
      subgoal using smap_shifted_eq by auto 
      subgoal for i by(erule allE[of _ "Suc i"], auto) . . . 


lemma Rst_r:"⋀k. Rst nds !! k = RR' (nds !! k, nds !! Suc k)"using Rst_correct by auto

(***)
(*For any ipath nds, we have that for i∈N RR(nds!i, nds!Suc i) ∈ Lang Taut⇩_R iff nds is descending *)

lemma list_swap:"k>0 ⟹ (p ## smap (λr. fst (the r)) r) !! k = fst (the (r !! (k-1))) " by (cases k, auto)
lemma Taut⇩_R_lang_in:"ipath nds ⟹ Rst nds ∈ NBA.language Taut⇩_R ⟷ (∃Ps. descentIpath nds Ps)"
proof(safe)
  assume ipath:"ipath nds"

  have k_edge:"⋀k. edge (nds !! k) (stl nds !! k)" using ipath unfolding ipath_def alw_holds2_iff_snth by auto

  show "Rst nds ∈ NBA.language Taut⇩_R ⟹ ∃Ps. descentIpath nds Ps"

  proof -
    assume "Rst nds ∈ NBA.language Taut⇩_R"
    then obtain r where run:"NBA.run Taut⇩_R (Rst nds ||| r) None"  and accept:"infs (λps. ∃p. ps = Some (p, Decr) ∧ (p, Decr) ∈ Q'⇩_s⇩_l) r" apply-by(erule nba.language_elim, auto)

    hence run':"⋀k. Rst nds !! k = RR' (nds !! k, nds !! Suc k) ∧ edge (nds !! k) (nds !! Suc k) ∧
        r !! k ∈ Δ⇩_s⇩_l' (Rst nds !! k) (if k = 0 then None else last (stake k r))"
      using k_edge unfolding Paut⇩_R_run_def by auto


  (*If we reach a point k where Decr occurs, then no future state j with j≥k can be q⇩₀*)
  have q⇩₀'_Decr:"⋀p k j. 0<k ⟹ r !! k = Some (p, Decr) ⟹ k ≤ j ⟹ r !! j ≠ q⇩₀"
    subgoal for p k j proof(induct "j - k" arbitrary: j)
      case 0
      then show ?case by auto
    next
      case (Suc xa)
      hence Suc':"⋀ j. 0 < k ⟹ xa = j - k ⟹ k ≤ j ⟹ r !! j ≠ q⇩₀" by auto
      obtain n where n:"j = Suc n" "xa = n - k" "k ≤ n" using Suc by(cases j,auto)
      show ?case 
        using Suc'[of n,OF Suc(3) n(2,3)] unfolding n
        using runE_Suc[OF run, of n] q⇩₀_notReachable[of "r !! n" "r !! Suc n"] by auto
    qed .

    have accept_from_notNone:"⋀n. ∃k≥n. ∃p. r !! k = Some (p, Decr) ∧ Some (p, Decr) ∈ Δ⇩_s⇩_l' (Rst nds !! k) (last (stake k r)) ∧ (last (stake k r)) ≠ None"
      subgoal for n
      using accept unfolding infs_snth
      apply-apply(erule allE[of _ "Suc n"], safe)
      subgoal for k p       using accept unfolding infs_snth
        apply-apply(erule allE[of _ "Suc k"], safe)
        subgoal for k' p' apply(intro exI[of _ k'] conjI exI[of _ p'])
          subgoal by auto
          subgoal by auto
          subgoal using run'[of k'] by auto
          subgoal using q⇩₀'_Decr[of k p "k'-1"] last_stake_i[of k' r] by auto . . . .


  obtain Ps where Ps:"Ps = fst (the (shd r)) ## smap (λr. fst (the r)) r" by auto

  have PsK:"⋀k. k>0 ⟹ Ps !! k = fst(the (r !!(k - Suc 0)))" subgoal for k unfolding Ps by(drule list_swap[of k "(fst (the (shd r)))" r], simp) .

  show "∃Ps. descentIpath nds Ps"
  apply(rule exI[of _ Ps], unfold descentIpath_iff_snth2, intro conjI)
  subgoal using accept_from_notNone[of "Suc 0"] apply safe
  subgoal for k p' a b apply(rule exI[of _ k], intro allI impI)
  subgoal for j proof(induct "j - k" arbitrary: j)
    case 0
    then have k:"k>0"  by auto
    hence last:"(last (stake k r)) = (r !! (k - 1))" using last_stake_i by auto
    also have j:"j>0" using 0 by auto
    show ?case using 0 unfolding last apply-apply(erule Δ⇩_s⇩_l'_elim)
      using PsK[OF j] PsK[of "Suc j"] by auto
  next
    case (Suc x)
    hence jk:"j ≠ 0" "k ≠ 0" "j > 0" "k > 0" "0 < Suc j" by auto
    then obtain n where j:"j = Suc n" by (cases j, auto)
    then have n_gr:"n > 0" "k ≤ n" using Suc by auto
    also have k_le:"k ≤ j - 1" using n_gr j by auto
    have nth_stake_szip:"r !! j ∈ Δ⇩_s⇩_l' (Rst nds !! j) (r !! (j-1))" using run'[of "j", unfolded last_stake_i[OF jk(3)]] jk by auto
    obtain a' b' where r_j_min:"(r !! (j-1)) = Some(a',b')" using q⇩₀'_Decr[of k p' "j-1", OF jk(4) Suc(4) k_le]  by auto
    show ?case
      subgoal using nth_stake_szip apply-apply(erule Δ⇩_s⇩_l'_elim)
        subgoal for p s p' s' unfolding Rst_r PsK[OF jk(3)] PsK[OF jk(5)] by (cases s', auto)
        subgoal using r_j_min by auto
        subgoal using r_j_min by auto . .  
  qed . .
  apply(rule allI)
  subgoal for i using accept_from_notNone[of "Suc(Suc i)"] apply clarify
    subgoal for k p apply(rule exI[of _ "k"], intro conjI)
      subgoal by auto
      using Suc_diff_1[of k] last_stake_i[of k r] PsK[of k] PsK[of "k-1"]
      unfolding Rst_r Ps apply-apply(erule Δ⇩_s⇩_l'_elim)
      by (auto,metis fst_eqD option.sel)  . . 
  qed
(*Converse*)
  fix Ps  

  {assume iDPath:"descentIpath nds Ps"
   have ev:"ev (alw (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Main ∨ RR (nd, P) (nd', P') Decr))) (nds ||| Ps)"and
      alw:"alw (ev (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Decr))) (nds||| Ps)"
     using iDPath[unfolded descentIpath_def2] by auto

   also have wf:"wfLabS nds Ps" using descentIpath_wfLabS[OF iDPath] by auto

   have hh:"⋀x y z i. (stl x!!i, stl y!!i, stl z!!i) ∈sset (x ||| y ||| z)" 
      by (metis snth_sset snth_szip stream.set_sel(2) szip.sel(2))
   define F⇩_s⇩_l where "F⇩_s⇩_l = (λx' Ps' i. (if RR (x' !! i, Ps' !! i) (stl x' !! i, stl Ps' !! i) Decr then Decr else Main))"
   define Ss where "Ss = (λx Ps. Main ## fToStream (F⇩_s⇩_l x Ps))"
   note Ss_defs = Ss_def F⇩_s⇩_l_def fToStream_def

   have Ss_i:"⋀k m. m < Suc k ⟹ (Ss (sdrop (Suc m) nds) (sdrop (Suc m) Ps) !! (Suc k - m)) = F⇩_s⇩_l nds Ps (Suc k)" using Suc_diff_le unfolding Ss_defs by auto

   obtain m where m:"(⋀n. n≥m ⟹ (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Main ∨ RR (nd, P) (nd', P') Decr)) (sdrop n (nds ||| Ps)))"
     using ev  unfolding ev_alw_iff_sdrop by auto

   have "⋀n. n≥m ⟹ (Rst nds !! n) (Ps !! n, Ps !! Suc n, Main) ∨ (Rst nds !! n) (Ps !! n, Ps !! Suc n, Decr)"
     subgoal for n by(drule m[of n], simp) .

  obtain i where i:"∀j≥i. Ps !! j ∈ PosOf (nds !! j)" using wf unfolding wfLabS_iff_snth by auto

  define m' where "m' = i + m" 
  hence m':"(⋀n. n≥m' ⟶ Ps !! n ∈ PosOf (nds !! n) ∧ ((Rst nds !! n) (Ps !! n, Ps !! Suc n, Main) ∨ (Rst nds !! n) (Ps !! n, Ps !! Suc n, Decr)))"
    using i m by auto

  have alw_dropm:"alw (ev (holds2 (λ(nd, P) (nd', P'). RR (nd, P) (nd', P') Decr))) (sdrop (Suc m') (nds ||| Ps))"
    using alw unfolding alw_ev_sdrop by auto


  define r where "r = replicate m' q⇩₀ @- smap Some ((sdrop (Suc m') Ps) ||| (Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps)))"

  have x_node':"⋀i. nds !! i ∈ Node" using ipath unfolding ipath_def alw_holdsS_iff_snth by auto

  have r_eq_q⇩₀':"⋀n. Suc n ≤ m' ⟷ r!!n = q⇩₀" 
    apply standard unfolding r_def
    subgoal using replicate_within_i by auto
    subgoal for n apply(rule ccontr, unfold not_le replicate_beyond_i) using x_node'[of "n"]  by auto .


  have r_neq_q⇩₀':"⋀n. Suc n > m' ⟷ r!!n = Some (Ps !! Suc n, Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps) !! (n-m'))" 
    apply standard
    subgoal unfolding r_def using replicate_beyond_i by auto 
    subgoal for n using r_eq_q⇩₀'[of n] by auto .


  have Rst_all:"⋀k. (Rst nds !!k) ∈ Σ" using k_edge unfolding Rst_r by auto

  have Psk_node:"⋀k. Ps !! k ∈ PosOf (nds !! k) ⟹ ∃x∈Node. Ps !! k ∈ PosOf x"
    using x_node' by auto
  have m'_inQ'⇩_s⇩_l:"⋀k x. k≥ m' ⟹ (Ps !! k, x) ∈ Q'⇩_s⇩_l"
    unfolding Q'⇩_s⇩_l_def using Psk_node  m' by auto


  have m_eq:"⋀k m. Suc k ≤ m ⟹ m < Suc (Suc k) ⟹ m = Suc k" by auto
  have Psn_gr:"⋀n. Suc n > m' ⟹ Ps !! (Suc n) = fst (the (r !! n))" using r_neq_q⇩₀' by auto
  have Ssn_gr:"⋀n. Suc n > m' ⟹ snd (the (r !! n)) = Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps) !! (n-m')" using r_neq_q⇩₀' by auto


  show"Rst nds ∈ NBA.language Taut⇩_R" 
  proof(rule nba.language[of q⇩₀ Taut⇩_R  _ r], unfold Taut⇩_R_accept Taut⇩_R_initp, safe)
    show "NBA.run Taut⇩_R (Rst nds ||| r) q⇩₀" 
    proof(unfold run_def', intro allI conjI) 
      fix k 
      show "Rst nds !! k ∈ Σ" using Rst_all by auto
  
      show "r !! k ∈ Δ⇩_s⇩_l' (Rst nds !! k) (last (None # map snd (stake k (Rst nds ||| r))))"
      proof(induct k)
        case 0
        have l:"(last (None # map snd (stake 0 (Rst nds ||| r))))  = None" by auto
        show ?case unfolding l 
          apply(cases m')
          subgoal apply(rule ssubst[of "r !!0" "Some (Ps !! (Suc 0), Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps) !! 0)"])
            subgoal  using r_neq_q⇩₀'[of 0] by auto
            subgoal apply(rule Δ⇩_s⇩_l'_intro_q0)
              subgoal using Rst_all[of 0] by auto
              subgoal using m'_inQ'⇩_s⇩_l[of "Suc 0"] by auto . . 
          subgoal apply(rule ssubst[of "r !!0" None]) 
            subgoal using r_eq_q⇩₀'[of 0] by auto
            apply(rule Δ⇩_s⇩_l'_q0_included) using Rst_all[of 0] by auto .
      next
        case (Suc k)
        then show ?case unfolding last_stake_szip apply-apply(erule Δ⇩_s⇩_l'_elim)
         (*Δ⇩_s⇩_l' 3*)       
          subgoal for p s p' s'  apply(rule Δ⇩_s⇩_l'_intro)
            subgoal using Rst_all[of "Suc k"] by auto
            subgoal apply(intro exI2[of _ "Ps !! Suc (Suc k)" "Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps) !! (Suc k - m')"] conjI)
              subgoal using r_eq_q⇩₀'[of k] r_neq_q⇩₀'[of "Suc k"] by auto
              subgoal using Psn_gr[of k] r_eq_q⇩₀'[of k] m'_inQ'⇩_s⇩_l[of "Suc k"] by auto
              subgoal using  m'[of "Suc k"] r_eq_q⇩₀'[of k] Ss_i Psn_gr unfolding F⇩_s⇩_l_def by auto .
            subgoal by auto .
          (*Δ⇩_s⇩_l' 2*)   
          subgoal for p s apply(rule Δ⇩_s⇩_l'_intro)
            subgoal using Rst_all[of "Suc k"] by auto
            subgoal apply(rule exI[of _ "Ps !! Suc (Suc k)"], intro exI[of _ "Ss (sdrop (Suc m') nds) (sdrop (Suc m') Ps) !! (Suc k - m')"] conjI)
              subgoal using r_eq_q⇩₀'[of k] r_neq_q⇩₀'[of "Suc k"] by auto
              subgoal by auto
              subgoal using  m'[of "Suc k"] r_eq_q⇩₀'[of k] Ss_i Psn_gr unfolding F⇩_s⇩_l_def by auto .
            subgoal by auto .
          (*Δ⇩_s⇩_l' 1*)   
          subgoal apply(rule Δ⇩_s⇩_l'_intro)
            subgoal using Rst_all[of "Suc k"] by auto
            subgoal by auto
            subgoal using le_less_linear[of "Suc (Suc k)" m'] apply-apply(erule disjE)
              subgoal using r_eq_q⇩₀'[of "Suc k"] by auto 
              subgoal using r_neq_q⇩₀'[of "Suc k"] m'_inQ'⇩_s⇩_l[of "Suc (Suc k)"] by auto . . .
      qed
    qed

    show "infs (λps. ∃p. ps = Some (p, Decr) ∧ (p, Decr) ∈ Q'⇩_s⇩_l) r"
      unfolding r_def alw_ev_shift infs_snth apply(clarify)
      subgoal for n using alw_dropm unfolding alw_ev_holds2_iff_snth
        apply-apply(erule allE[of _ "n + i"], clarify)
        subgoal for j x y xa ya apply(intro exI[of _ "Suc j"] conjI)
          subgoal by auto
          subgoal apply(intro exI[of _ ya] conjI)
            subgoal unfolding Ss_defs by auto
            subgoal using i RR_PosOfD' unfolding Q'⇩_s⇩_l_def by fastforce . . . .
  qed}
qed

(*Trivial auxillary results required*)
lemma alpha_subseq_PTaut⇩_R: "nba.alphabet Paut⇩_R ⊆ nba.alphabet Taut⇩_R" by simp
(*PATH AUTO FINITE NODES*)

lemma Paut⇩_R_subseq_rule:"(⋀r. ∀x∈Node. last (map snd r) ≠ Some x ⟹
         r ≠ [] ⟹ NBA.path Paut⇩_R r None ⟹ last (map snd r) = None) ⟹
(⋃p∈{p. p ∈ nba.initial Paut⇩_R}. {last (p # map snd r) |r. NBA.path Paut⇩_R r p})
    ⊆ {r. r = None ∨ (∃x∈Node. r = Some x)}" by auto


lemma Paut⇩_R_node_subseq:"NBA.nodes Paut⇩_R ⊆ {r. r = None ∨ (∃x∈ Node. r = Some x)}" 
  unfolding nba.nodes_alt_def nba.reachable_alt_def nba.target_alt_def nba.states_alt_def 
  apply(rule Paut⇩_R_subseq_rule)
  subgoal premises p for r using p(3,1-2) apply(induct rule: nba.path.induct)
    subgoal by auto
    subgoal for a p by (cases p,  auto simp: RR_PosOfD' split: if_splits) . . 


lemma finite_Nodes_Paut⇩_R:"finite (NBA.nodes Paut⇩_R)" 
  apply(rule rev_finite_subset[OF _ Paut⇩_R_node_subseq]) using finite_Node_opt by auto 

(*TRACE AUTO FINITE NODES*)

lemma Taut⇩_R_subseq_rule:"(⋀r.  ∀a. (∀x∈Node. a ∉ PosOf x) ∨ (∀b. last (map snd r) ≠ Some (a, b)) ⟹
         r ≠ [] ⟹ NBA.path Taut⇩_R r None ⟹ last (map snd r) = None)
  ⟹ (⋃p∈{p. p ∈ nba.initial Taut⇩_R}. {last (p # map snd r) |r. NBA.path Taut⇩_R r p})
    ⊆ {r. r = None ∨ (∃x∈{(p, s)| p s. p ∈ (⋃v∈Node. PosOf v)}. r = Some x)}" by auto


(*Theorem 5.4*)
theorem SLA_Criterion:"InfiniteDescent ⟷ NBA.language Paut⇩_R ⊆ NBA.language Taut⇩_R"
  apply standard
  subgoal unfolding subset_iff Paut⇩_R_lang_in InfiniteDescent_def apply clarify
    subgoal for Ri nds apply(erule allE[of _ nds], safe)
      by(drule Taut⇩_R_lang_in,unfold Rst_correct[of Ri nds,symmetric], auto) . 
  subgoal unfolding InfiniteDescent_def apply(clarify)
    subgoal for nds 
      apply(unfold subset_iff Paut⇩_R_lang_in)
      by(erule allE[of _ "Rst nds"], unfold Taut⇩_R_lang_in, auto) . .

end
end