Theory Usable_Rules_Complexity

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2014, 2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Usable_Rules_Complexity
imports
  QTRS.Q_Relative_Rewriting
  QTRS.Complexity
  "Check-NT.Innermost_Usable_Rules"
  Usable_Replacement_Map
begin

context 
  fixes US :: "'f sig"
  and U :: "('f,'v)trs"
  and R :: "('f,'v)trs"
  and Q :: "('f,'v)terms"
  and nfs :: bool
begin
definition usable_symbols_rule_closed :: "('f,'v)rule ⇒ bool" where
  "usable_symbols_rule_closed lr ≡ case lr of (l,r) ⇒
    funas_term l ⊆ US ⟶ funas_term r ⊆ US"

definition usable_symbols_closed :: "bool" where
  "usable_symbols_closed ≡ ∀ lr ∈ U. usable_symbols_rule_closed lr"

definition U_usable :: bool where
  "U_usable ≡ ∀ lr ∈ R. funas_term (fst lr) ⊆ US ⟶ lr ∈ U"

context
  assumes U_usable usable_symbols_closed 
  and wf: "⋀ l r. (l,r) ∈ U ⟹ vars_term r ⊆ vars_term l"
begin

lemma only_usable_step: assumes sUS: "funas_term s ⊆ US"
  and R': "R' ⊆ R"
  and step: "(s,t) ∈ qrstep nfs Q R'"
  shows "(s,t) ∈ qrstep nfs Q (R' ∩ U) ∧ funas_term t ⊆ US"
proof -
  from qrstepE[OF step]
  obtain C σ l r where nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and
      lr: "(l, r) ∈ R'" and 
      s: "s = C⟨l ⋅ σ⟩" and 
      t: "t = C⟨r ⋅ σ⟩" and 
      nfs: "NF_subst nfs (l, r) σ Q" .
  note sUS = sUS[unfolded s]
  from sUS have l: "funas_term l ⊆ US" by (auto simp: funas_term_subst)
  with ‹U_usable›[unfolded U_usable_def] lr R' have lrU: "(l,r) ∈ U" by auto
  with nf lr s t nfs have step: "(s,t) ∈ qrstep nfs Q (R' ∩ U)" by auto
  from wf[OF lrU] have vars: "vars_term r ⊆ vars_term l" .
  from ‹usable_symbols_closed›[unfolded usable_symbols_closed_def] lrU
  have "usable_symbols_rule_closed (l,r)" by auto  
  from this[unfolded usable_symbols_rule_closed_def] l have "funas_term r ⊆ US" by auto
  with vars sUS have "funas_term t ⊆ US" unfolding t
    by (force simp: funas_term_subst)
  with step show ?thesis by blast
qed

lemma usable_rules_complexity: assumes S: "S ⊆ R" and W: "W ⊆ R" 
  and sig: "set (get_signature_of_cm cm) ⊆ US"
  and bound: "deriv_bound_measure_class 
    (relto (qrstep nfs Q (S ∩ U)) (qrstep nfs Q (W ∩ U)))
    cm cc" (is "deriv_bound_measure_class ?U cm cc")
  shows "deriv_bound_measure_class 
    (relto (qrstep nfs Q S) (qrstep nfs Q W))
    cm cc" (is "deriv_bound_measure_class ?P cm cc")
proof -
  note d = deriv_bound_measure_class_def deriv_bound_rel_class_def deriv_bound_rel_def
  from bound[unfolded d] obtain f where 
    f: "f ∈ O_of cc" and
    bound: "⋀ n t. t ∈ terms_of_nat cm n ⟹ deriv_bound ?U t (f n)" 
    by auto
  show ?thesis unfolding d
  proof (intro exI[of _ f] conjI[OF f] allI impI)
    fix n t
    assume t: "t ∈ terms_of_nat cm n"
    with get_signature_of_cm[of cm n] sig have tUS: "funas_term t ⊆ US" by auto
    note d = deriv_bound_def
    from bound[OF t] have bound: "deriv_bound ?U t (f n)" .
    show "deriv_bound ?P t (f n)" unfolding d
    proof
      assume "∃ s. (t,s) ∈ ?P^^(Suc (f n))"
      then obtain s where steps: "(t,s) ∈ ?P^^(Suc (f n))" by auto
      let ?p = "λ t. funas_term t ⊆ US"
      let ?s = "Collect ?p"
      let ?R = "qrstep nfs Q R"
      let ?S = "qrstep nfs Q S"
      let ?W = "qrstep nfs Q W"
      from tUS have tUS: "t ∈ ?s" by auto
      have "(t,s) ∈ ?U^^(Suc (f n))"
      proof (rule abstract_closure_twice.AA_steps_imp_BB_steps[of _ _ ?R ?s ?p, OF _ tUS steps],
        unfold_locales)
        show "?S ⊆ ?R^*" using qrstep_mono[OF S subset_refl, of nfs Q] by auto
        show "?W ⊆ ?R^*" using qrstep_mono[OF W subset_refl, of nfs Q] by auto
        show "⋀ a b. funas_term a ⊆ US ⟹ (a, b) ∈ ?S ⟹ (a, b) ∈ qrstep nfs Q (S ∩ U)"
          using only_usable_step[OF _ S] by blast
        show "⋀ a b. funas_term a ⊆ US ⟹ (a, b) ∈ ?W ⟹ (a, b) ∈ qrstep nfs Q (W ∩ U)"
          using only_usable_step[OF _ W] by blast
        fix s t 
        assume s: "s ∈ ?s" and st: "(s,t) ∈ ?R^*" 
        from st show "?p t"
        proof (induct)
          case (step t u)
          from only_usable_step[OF step(3) _ step(2)] show ?case by auto
        qed (insert s, auto)
      qed
      with bound[unfolded d] show False by auto
    qed
  qed
qed
end
end

context R_Q_U_ecap
begin

context
  fixes S W :: "('f,string)trs"
  and C D :: "('f × nat)list"
  and cm :: "('f,string)complexity_measure"
  assumes 
      R: "S ∪ W ⊆ R"
  and wf: "wf_trs R"
  and rt: "cm = Runtime_Complexity C D"
  and C: "⋀ c. c ∈ set C ⟹ ¬ defined R c"
  and init: "⋀ l r. (l,r) ∈ R ⟹ the (root l) ∈ set D ⟹ 
    ⋃ (funas_term ` set (args l)) ⊆ set C ⟹ (l,r) ∈ U"
begin

(* store info for usable rules for complexity *)
definition "urc_info t n nfs ts sel m s l r σ lr p τ ≡ relto_fun (qrstep nfs Q S) (qrstep nfs Q W) (Suc n) ts sel m (t, s)
    ∧ ts 0 = l ⋅ σ ∧ ts (Suc 0) = r ⋅ σ ∧ (l,r) ∈ U ∧ lr 0 = (l,r)
    ∧ set (args l) ⋅⇩s⇩e⇩t σ ⊆ NFQ ∧ σ ` vars_term r ⊆ NFQ 
    ∧ (∀ i < m. (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (τ i))
    ∧ (∀ i < m. vars_term (snd (lr i)) ⊆ vars_term (fst (lr i)) ∧ is_Fun (fst (lr i)))
    ∧ (∀ i < m. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i})
    ∧ (∀ i < m. lr i ∈ (if sel i then S else W))"

lemma get_step_urc_info: assumes t: "t ∈ terms_of_nat cm n'"
  and steps: "∃ s. (t,s) ∈ ((relto (qrstep nfs Q S) (qrstep nfs Q W)))^^(Suc n)"
  shows "∃ ts sel m s l r σ lr p τ. urc_info t n nfs ts sel m s l r σ lr p τ"
proof -
  let ?P = "relto (qrstep nfs Q S) (qrstep nfs Q W)"
  from t[unfolded rt] obtain g ss where 
      tg: "t = Fun g ss" and g: "(g,length ss) ∈ set D" and 
      ss: "⋀ ti. ti ∈ set ss ⟹ funas_term ti ⊆ set C" by (force simp: funas_args_term_def)
  from steps obtain s where steps: "(t,s) ∈ ?P^^(Suc n)" by auto
  from reltos_into_relto_fun[OF this] obtain ts sel m where 
    rtf: "relto_fun (qrstep nfs Q S) (qrstep nfs Q W) (Suc n) ts sel m (t, s)" by blast      
  note steps = relto_funD[OF rtf]
  let ?R = "λ i. if sel i then S else W"
  let ?RU = "λ i. if sel i then S ∩ U else W ∩ U"
  {
    fix i
    assume "i < m"
    from steps(3-4)[OF this, unfolded qrstep_rule_conv[where R = S] qrstep_rule_conv[where R = W]]
    have "∃ lr ∈ ?R i. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr}" by auto
  }
  hence "∀ i. ∃ lr. i < m ⟶ lr ∈ ?R i ∧ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr}" by blast
  from choice[OF this] obtain lr where lr: "⋀ i. i < m ⟹ lr i ∈ ?R i" 
    and step: "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i}" by blast+
  from lr R have lrR: "⋀ i. i < m ⟹ lr i ∈ R" by (force split: if_splits)
  {
    fix i
    assume i: "i < m"
    from step[OF i, unfolded qrstep_qrstep_r_p_s_conv] obtain lr' p τ
    where "(ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q {lr i} lr' p τ" by auto
    with lrR[OF i]
    have "(ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) p τ" unfolding qrstep_r_p_s_def by auto
    hence "∃ p τ. (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) p τ" by blast
  }
  hence "∀ i. ∃ p τ. i < m ⟶ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) p τ" by blast
  from choice[OF this] obtain p where "∀ i. ∃ τ. i < m ⟶ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) τ" by blast
  from choice[OF this] obtain τ where 
    step': "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (τ i)" by blast
  obtain l r where lr0: "lr 0 = (l,r)" by force
  from steps have 0: "0 < m" by auto      
  from lrR[OF 0] lr0 have lrR0: "(l,r) ∈ R" by auto
  from step[OF 0] steps(1) lr0 have "(t, ts 1) ∈ qrstep nfs Q {(l,r)}" by simp
  then obtain C' σ where tl: "t = C'⟨l ⋅ σ⟩" and tr: "ts 1 = C'⟨r ⋅ σ⟩" 
    and Q: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" by auto
  from wf_trs_imp_lhs_Fun[OF wf lrR0] obtain f ls where l: "l = Fun f ls"
    by auto
  have C': "C' = □"
  proof (cases C')
    case (More h bef D' aft)
    from tl[unfolded this tg] have "D'⟨l ⋅ σ⟩ ∈ set ss" by auto
    from ss[OF this] have lC: "funas_term (l ⋅ σ) ⊆ set C" by auto
    from l lrR0 lr0 have "(Fun f ls, r) ∈ R" by auto 
    hence df: "defined R (f,length ls)" unfolding defined_def by auto
    from lC l have "(f,length ls) ∈ set C" by (auto simp: funas_term_subst)
    from C[OF this] df show ?thesis by simp
  qed simp
  with tl tr steps have tl: "ts 0 = l ⋅ σ" and tr: "ts (Suc 0) = r ⋅ σ" by auto
  let ?ts = "λ i. ts (Suc i)"
  let ?lr = "λ i. lr (Suc i)"
  let ?p = "λ i. p (Suc i)"
  let ?τ = "λ i. τ (Suc i)"
  from steps obtain m' where m: "m = Suc m'" by (cases m, auto)
  hence i: "⋀ i. i < m' ⟹ Suc i < m" by auto
  from Q[folded NF_terms_args_conv] have lQ: "set (args l) ⋅⇩s⇩e⇩t σ ⊆ NFQ" unfolding l by auto
  {
    fix x
    assume "x ∈ vars_term r"
    with wf lrR0 have "x ∈ vars_term l" by (auto simp: wf_trs_def)
    hence "l ⊳ Var x" unfolding l by force
    from supt_subst[OF this, of σ] Q have "σ x ∈ NFQ" by auto
  }
  hence rQ: "σ ` vars_term r ⊆ NFQ" by auto
  {
    fix i
    assume "i < m" 
    from wf lrR[OF this] 
    have "vars_term (snd (lr i)) ⊆ vars_term (fst (lr i))" "is_Fun (fst (lr i))"
      unfolding wf_trs_def by (cases "lr i", force)+
  } note wf = this
  from tl l steps(1) tg have lg: "l ⋅ σ = Fun g ss" by simp
  from lg l g have lD: "the (root l) ∈ set D" by auto
  from lg l ss have argsC: "⋃(funas_term ` set (args l)) ⊆ set C" by (force simp: funas_term_subst)
  have lrU0: "(l,r) ∈ U"
    by (rule init[OF lrR0 lD argsC]) 
  show ?thesis unfolding urc_info_def
    by (intro exI conjI allI impI, rule rtf, rule tl, rule tr, rule lrU0, rule lr0, 
      rule lQ, rule rQ, rule step', insert step lr wf, auto)
qed  

lemma usable_rules_innermost_complexity_urm: assumes 
      U: "⋀ l r. (l,r) ∈ U ⟹ is_ur_closed_term_mv μ (set (args l)) r"
  and URM: "usable_replacement_map μ (terms_of cm) nfs R Q R"
  and bound: "deriv_bound_measure_class 
    (relto (qrstep nfs Q (S ∩ U)) (qrstep nfs Q (W ∩ U)))
    cm cc" (is "deriv_bound_measure_class ?U cm cc")
  shows "deriv_bound_measure_class 
    (relto (qrstep nfs Q S) (qrstep nfs Q W))
    cm cc" (is "deriv_bound_measure_class ?P cm cc")
proof -
  note d = deriv_bound_measure_class_def deriv_bound_rel_class_def deriv_bound_rel_def
  from bound[unfolded d] obtain f where 
    f: "f ∈ O_of cc" and
    bound: "⋀ n t. t ∈ terms_of_nat cm n ⟹ deriv_bound ?U t (f n)" 
    by auto
  show ?thesis unfolding d
  proof (intro exI[of _ f] conjI[OF f] allI impI)
    fix n t
    assume t: "t ∈ terms_of_nat cm n"
    from bound[OF t] have bound: "deriv_bound ?U t (f n)" .
    note d = deriv_bound_def
    show "deriv_bound ?P t (f n)" unfolding d
    proof
      assume "∃ s. (t,s) ∈ ?P^^(Suc (f n))"
      from get_step_urc_info[OF t this] obtain ts sel m s l r σ lr p τ where
        info: "urc_info t (f n) nfs ts sel m s l r σ lr p τ" by auto
      from info[unfolded urc_info_def] have
        rtf: "relto_fun (qrstep nfs Q S) (qrstep nfs Q W) (Suc (f n)) ts sel m (t, s)" 
        and tl: "ts 0 = l ⋅ σ" and tr: "ts (Suc 0) = r ⋅ σ" and lrU0: "(l,r) ∈ U" 
        and lr0: "lr 0 = (l,r)" 
        and lQ: "set (args l) ⋅⇩s⇩e⇩t σ ⊆ NFQ" and rQ: "σ ` vars_term r ⊆ NFQ"
        and step': "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (τ i)" 
        and wf: "⋀ i. i < m ⟹ vars_term (snd (lr i)) ⊆ vars_term (fst (lr i)) ∧ is_Fun (fst (lr i))" 
        and step: "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i}"
        and lr: "⋀ i. i < m ⟹ lr i ∈ (if sel i then S else W)" by auto
      note steps = relto_funD[OF rtf]
      let ?R = "λ i. if sel i then S else W"
      let ?RU = "λ i. if sel i then S ∩ U else W ∩ U"
      let ?ts = "λ i. ts (Suc i)"
      let ?lr = "λ i. lr (Suc i)"
      let ?p = "λ i. p (Suc i)"
      let ?τ = "λ i. τ (Suc i)"
      from steps obtain m' where m: "m = Suc m'" by (cases m, auto)
      hence i: "⋀ i. i < m' ⟹ Suc i < m" by auto
      {
        fix i
        assume im': "i < m'"
        with m have im: "Suc i ≤ m" "Suc i < m" by auto
        let ?ti = "ts (Suc i)"  
        let ?pi = "p (Suc i)"
        have "lr (Suc i) ∈ U"
        proof (rule is_ur_closed_term_main_af[of m' ?ts nfs ?lr ?p ?τ, OF step'[OF i] wf[OF i] rQ tr lQ U U[OF lrU0] _ im'])
          have "(t, ?ti) ∈ (qrstep nfs Q R)⇧*"
            by (rule relto_fun_intermediate[OF qrstep_mono qrstep_mono rtf im(1)], insert R, auto)
          with t have "?ti ∈ (qrstep nfs Q R)⇧* `` terms_of cm" by (auto simp: terms_of)
          with URM[unfolded usable_replacement_map_def] 
          have af: "?ti ∈ af_nf_compatible_terms μ (qrstep nfs Q R)" by auto
          def C ≡ "ctxt_of_pos_term ?pi ?ti"
          from qrstep_r_p_s_conv[OF step'[OF im(2)]] have hp: "?pi = hole_pos C"
            and ti: "?ti = C⟨fst (lr (Suc i)) ⋅ τ (Suc i)⟩" unfolding C_def by auto
          from step'[OF im(2)] have step: "(fst (lr (Suc i)) ⋅ τ (Suc i), snd (lr (Suc i)) ⋅ τ (Suc i))
            ∈ qrstep nfs Q R" unfolding qrstep_r_p_s_def by auto
          with af[unfolded af_nf_compatible_terms_def] 
          show "af_regarded_pos μ ?ti ?pi" unfolding ti hp by auto
        qed auto
      } note lrU = this
      have "relto_fun (qrstep nfs Q (S ∩ U)) (qrstep nfs Q (W ∩ U)) (Suc (f n)) ts sel m (t, s)"
      proof (rule relto_fun[OF steps(1-2) _ steps(5-6)])
        fix i
        assume i: "i < m"
        hence "lr i ∈ U" using lrU[of "i - 1"] lrU0 lr0 m by (cases i, auto)
        with step'[OF i] lr[OF i] have "lr i ∈ ?RU i" by auto
        with step[OF i] have "(ts i, ts (Suc i)) ∈ qrstep nfs Q (?RU i)" 
          unfolding qrstep_rule_conv[where R = "?RU i"] by auto
        thus "(sel i ⟶ (ts i, ts (Suc i)) ∈ qrstep nfs Q (S ∩ U)) ∧
         (¬ sel i ⟶ (ts i, ts (Suc i)) ∈ qrstep nfs Q (W ∩ U))"
         by (cases "sel i", auto)
      qed
      from relto_fun_into_reltos[OF this]
      have "(t,s) ∈ ?U^^(Suc (f n))" .
      with bound[unfolded d] show False by blast
    qed
  qed
qed

lemma usable_rules_innermost_complexity: assumes 
      U: "⋀ l r. (l,r) ∈ U ⟹ is_ur_closed_term_mv full_af (set (args l)) r"
  and bound: "deriv_bound_measure_class 
    (relto (qrstep nfs Q (S ∩ U)) (qrstep nfs Q (W ∩ U)))
    cm cc" 
  shows "deriv_bound_measure_class 
    (relto (qrstep nfs Q S) (qrstep nfs Q W))
    cm cc" 
  by (rule usable_rules_innermost_complexity_urm[OF U _ bound], auto)

text ‹in the following proof we do not make use of the fact that NS_ord
   is monotone in all arguments, which is enforced by the rp-precondition on
   @{term cpx_ce_af_redtriple_order}}›
lemma usable_rules_innermost_complexity_urm_redpair: assumes 
      compatR: "S ∩ U ⊆ S_ord" "W ∩ U ⊆ NS_ord"
  and af: "af_monotone μ⇩S S_ord" "af_monotone μ⇩w NS_ord"
  and cpx: "cpx_class cm cc"
  and URMS: "usable_replacement_map μ⇩S (terms_of cm) nfs R Q S"
  and URMW: "usable_replacement_map μ⇩w (terms_of cm) nfs R Q W"
  and U: "⋀ l r. (l,r) ∈ U ⟹ is_ur_closed_term_mv μ⇩S (set (args l)) r"
  and Uπ: "⋀ l r. (l,r) ∈ U ⟹ is_ur_closed_term_mv (af_inter π μ⇩w) (set (args l)) r"
  and rp: "cpx_ce_af_redtriple_order S_ord NS_ord NST_ord π μ cpx_class"
  shows "deriv_bound_measure_class 
    (relto (qrstep nfs Q S) (qrstep nfs Q W))
    cm cc" (is "deriv_bound_measure_class ?P cm cc")
proof -
  interpret cpx_ce_af_redtriple_order S_ord NS_ord NST_ord π μ cpx_class by fact
  note d = deriv_bound_measure_class_def deriv_bound_rel_class_def deriv_bound_rel_def
  from cpx_class[OF cpx] have bound: "deriv_bound_measure_class S_ord cm cc" .
  from bound[unfolded d] obtain f where 
    f: "f ∈ O_of cc" and
    bound: "⋀ n t. t ∈ terms_of_nat cm n ⟹ deriv_bound S_ord t (f n)" 
    by auto
  show ?thesis unfolding d
  proof (intro exI[of _ f] conjI[OF f] allI impI)
    fix n t
    assume t: "t ∈ terms_of_nat cm n"
    from bound[OF t] have bound: "deriv_bound S_ord t (f n)" .
    note d = deriv_bound_def
    show "deriv_bound ?P t (f n)" unfolding d
    proof
      assume "∃ s. (t,s) ∈ ?P^^(Suc (f n))"
      from get_step_urc_info[OF t this] obtain ts sel m s l r σ lr p τ where
        info: "urc_info t (f n) nfs ts sel m s l r σ lr p τ" by auto
      from info[unfolded urc_info_def] have
        rtf: "relto_fun (qrstep nfs Q S) (qrstep nfs Q W) (Suc (f n)) ts sel m (t, s)" 
        and tl: "ts 0 = l ⋅ σ" and tr: "ts (Suc 0) = r ⋅ σ" and lrU0: "(l,r) ∈ U" 
        and lr0: "lr 0 = (l,r)" 
        and lQ: "set (args l) ⋅⇩s⇩e⇩t σ ⊆ NFQ" and rQ: "σ ` vars_term r ⊆ NFQ"
        and step': "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (τ i)" 
        and wf: "⋀ i. i < m ⟹ vars_term (snd (lr i)) ⊆ vars_term (fst (lr i)) ∧ is_Fun (fst (lr i))" 
        and step: "⋀ i. i < m ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i}"
        and lr: "⋀ i. i < m ⟹ lr i ∈ (if sel i then S else W)" by auto
      note steps = relto_funD[OF rtf]
      let ?R = "λ i. if sel i then S else W"
      let ?RU = "λ i. if sel i then S ∩ U else W ∩ U"
      let ?ts = "λ i. ts (Suc i)"
      let ?lr = "λ i. lr (Suc i)"
      let ?p = "λ i. p (Suc i)"
      let ?τ = "λ i. τ (Suc i)"
      from steps obtain m' where m: "m = Suc m'" by (cases m, auto)
      hence i: "⋀ i. i < m' ⟹ Suc i < m" by auto
      {
        assume "sel 0"
        with lr[of 0] m have "lr 0 ∈ S" by auto
        with lr0 lrU0 have "(l,r) ∈ S ∩ U" by auto
        with compatR have "(l,r) ∈ S_ord" by auto
        from subst.closedD[OF subst_S this, of σ] tl tr have "(ts 0, ts (Suc 0)) ∈ S_ord" by auto
      } note S_ord_0 = this
      {
        assume "¬ sel 0"
        with lr[of 0] m have "lr 0 ∈ W" by auto
        with lr0 lrU0 have "(l,r) ∈ W ∩ U" by auto
        with compatR have "(l,r) ∈ NS_ord" by auto
        from subst.closedD[OF subst_NS this, of σ] tl tr have "(ts 0, ts (Suc 0)) ∈ NS_ord" by auto
      } note NS_ord_0 = this
      {
        fix i
        assume im': "i < m'"
        with m have im: "Suc i ≤ m" "Suc i < m" by auto
        let ?ti = "ts (Suc i)"  
        let ?pi = "p (Suc i)"
        let ?C = "ctxt_of_pos_term (?p i) (?ts i)"
        def C ≡ ?C
        from qrstep_r_p_s_conv[OF step'[OF im(2)]] 
          have tsSi: "?ts (Suc i) = C⟨snd (?lr i) ⋅ ?τ i⟩" and pi: "?p i ∈ poss (?ts i)"
          and hp: "?pi = hole_pos C"
          and tsi: "?ts i = C ⟨fst (?lr i) ⋅ ?τ i⟩" unfolding C_def by auto
        have "(t, ?ti) ∈ (qrstep nfs Q R)⇧*"
          by (rule relto_fun_intermediate[OF qrstep_mono qrstep_mono rtf im(1)], insert R, auto)
        with t have ti1: "?ti ∈ (qrstep nfs Q R)⇧* `` terms_of cm" by (auto simp: terms_of)
        have piC: "?pi = hole_pos C" unfolding C_def using pi by auto
        {
          assume "sel (Suc i)"
          with lr[OF im(2)] have lrS: "lr (Suc i) ∈ S" by auto
          {
            from ti1 URMS[unfolded usable_replacement_map_def] 
            have af: "?ti ∈ af_nf_compatible_terms μ⇩S (qrstep nfs Q S)" by auto
            from step'[OF im(2)] lrS have step: "(fst (lr (Suc i)) ⋅ τ (Suc i), snd (lr (Suc i)) ⋅ τ (Suc i))
              ∈ qrstep nfs Q S" unfolding qrstep_r_p_s_def by auto
            with af[unfolded af_nf_compatible_terms_def] 
            have "af_regarded_pos μ⇩S ?ti ?pi" unfolding tsi hp by auto
          } note rμ = this
          have "?lr i ∈ U"
            by (rule is_ur_closed_term_main_af[of m' ?ts nfs ?lr ?p ?τ, OF step'[OF i] wf[OF i] rQ tr lQ U U[OF lrU0] rμ im'], auto)
          with lrS have "?lr i ∈ S ∩ U" by auto
          with compatR have S: "?lr i ∈ S_ord" by auto
          with subst.closedD[OF subst_S] have "(fst (?lr i) ⋅ ?τ i, snd (?lr i) ⋅ ?τ i) ∈ S_ord" by auto
          from af_monotone_af_regarded_posD[OF af(1) rμ[unfolded tsi piC] this]
          have "(?ts i, ?ts (Suc i)) ∈ S_ord" unfolding tsi tsSi .
        }
        moreover
        {
          assume "¬ sel (Suc i)"
          with lr[OF im(2)] have lrW: "lr (Suc i) ∈ W" by auto
          have "(?ts i, ?ts (Suc i)) ∈ NS_ord"
          proof (cases "af_regarded_pos π ?ti ?pi")
            case False
            from af_compatible_af_regarded_ctxt[OF af_compat wm_NS False[unfolded tsi piC]]
            show ?thesis unfolding tsi tsSi .
          next
            case True
            {
              from ti1 URMW[unfolded usable_replacement_map_def] 
              have af: "?ti ∈ af_nf_compatible_terms μ⇩w (qrstep nfs Q W)" by auto
              from step'[OF im(2)] lrW have step: "(fst (lr (Suc i)) ⋅ τ (Suc i), snd (lr (Suc i)) ⋅ τ (Suc i))
                ∈ qrstep nfs Q W" unfolding qrstep_r_p_s_def by auto
              with af[unfolded af_nf_compatible_terms_def] 
              have "af_regarded_pos μ⇩w ?ti ?pi" unfolding tsi hp by auto
            } note rμ = this
            with True have afi: "af_regarded_pos (af_inter π μ⇩w) ?ti ?pi"
              unfolding af_regarded_pos_af_inter by blast
            have "?lr i ∈ U" 
              by (rule is_ur_closed_term_main_af[of m' ?ts nfs ?lr ?p ?τ, 
                  OF step'[OF i] wf[OF i] rQ tr lQ Uπ Uπ[OF lrU0] afi im'], auto)
            with lrW have "?lr i ∈ W ∩ U" by auto
            with compatR have NS: "?lr i ∈ NS_ord" by auto
            with subst.closedD[OF subst_NS] have "(fst (?lr i) ⋅ ?τ i, snd (?lr i) ⋅ ?τ i) ∈ NS_ord" by auto
            from af_monotone_af_regarded_posD[OF af(2) rμ[unfolded tsi piC] this]
            show "(?ts i, ?ts (Suc i)) ∈ NS_ord" unfolding tsi tsSi .
          qed
        }
        ultimately 
        have "sel (Suc i) ⟹ (?ts i, ?ts (Suc i)) ∈ S_ord"
             "¬ sel (Suc i) ⟹ (?ts i, ?ts (Suc i)) ∈ NS_ord" by blast+
      } note later = this
      {
        fix i
        assume i: "i < m"
        have "(sel i ⟶ (ts i, ts (Suc i)) ∈ S_ord) ∧ (¬ sel i ⟶ (ts i, ts (Suc i)) ∈ NS_ord)"
        proof (cases i)
          case 0
          with S_ord_0 NS_ord_0 show ?thesis by auto
        next
          case (Suc j)
          with later[of j] i[unfolded m] show ?thesis by auto
        qed
        hence "sel i ⟹ (ts i, ts (Suc i)) ∈ S_ord" "¬ sel i ⟹ (ts i, ts (Suc i)) ∈ NS_ord" by auto
      } note main = this      
      have "relto_fun S_ord NS_ord (Suc (f n)) ts sel m (t, s)"
        by (rule relto_fun[OF steps(1-2) _ steps(5-6)], insert main, auto)
      from relto_fun_into_reltos[OF this, unfolded order_simps]
      have "(t,s) ∈ S_ord^^(Suc (f n))" .
      with bound[unfolded d] show False by blast
    qed
  qed
qed

end
end
end