Theory Semantic_Labeling_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Semantic_Labeling_Impl
imports 
  Semantic_Labeling
  QTRS.QDP_Framework_Impl
  "Check-NT.Q_Restricted_Rewriting_Impl"
begin

type_synonym ('f,'v)sl_check1 =
  "('f,'v)term list ⇒ ('f,'v)term list ⇒ shows check"

type_synonym ('f,'v)sl_check2 =
  "('f,'v)rules ⇒ ('f,'v)rules ⇒ shows check"

type_synonym ('f,'v)sl_check2s =
  "('f,'v)trs ⇒ ('f,'v)rules ⇒ shows check"

type_synonym ('f,'v)sl_check0 =
  "('f,'v)rules ⇒ shows check"

type_synonym ('f,'v)splitter = "('f,'v)rules ⇒ 
  ('f,'v)trs ⇒ (('f,'v)rules ×  ('f,'v)rules ×  ('f,'v)rules)"

definition quasi_splitter :: "('f,'f,'l)ldecompose ⇒ ('f,'v)splitter"
  where "quasi_splitter LD lAll uRw ≡ let 
  unlab = (λlf. fst (LD lf));
  la = map (λr. (r,map_funs_rule unlab r)) lAll;
  (D,nD) = partition (λ(r,ur). fst ur = snd ur ∧ fst r ≠ snd r) la;
  (Rw,R) = partition (λ(r,ur). ur ∈ uRw) nD
  in (map fst R,map fst Rw,map fst D)"

definition model_splitter :: "('f,'f,'l)ldecompose ⇒ ('f,'v)splitter"
  where "model_splitter LD lAll uRw ≡ let 
  unlab = (λlf. fst (LD lf));
  la = map (λr. (r,map_funs_rule unlab r)) lAll;
  (Rw,R) = partition (λ(r,ur). ur ∈ uRw) la
  in (map fst R,map fst Rw,[])"

definition check_sl_Q :: "('f ⇒ ('f × 'l)) ⇒ ('f::show, 'v::show) sl_check1"
where
  "check_sl_Q LD lQ Q =
    (let u = (λl. fst (LD l)) in 
    check_allm (λ lq. check (
      let mlq = map_funs_term u lq in
      (∃ q ∈ set Q. matches mlq q ∧ matches q mlq))
      (shows ''unlabeling '' +@+ shows_term lq +@+ shows '' yields a term not in Q'')) lQ)"
(* 
  remark: just demanding matches mlq q does not suffice to achieve check_sl_Q lemma!
   consider Q = {f(x,x)} lQ = {f_1(a_1,a_2)}.
   Then mlq = f(a,a) which is an instance of f(x,x), so the check would be satisfied,
   but f_1(a_1,a_2) is a normal form w.r.t. lab_lhss_all Q, but not w.r.t. lQ
*)

lemma check_sl_Q:
  assumes check: "isOK(check_sl_Q LD lQ Q)"
  shows "NF_terms (set lQ) ⊇ NF_terms (lab_lhss_all LD (set Q))"
proof(rule NF_vars_subset, rule)
  fix q'
  assume q': "q' ∈ set lQ"
  let ?f = "(λl. fst (LD l))"
  let ?m = "map_funs_term ?f"
  from check[unfolded check_sl_Q_def Let_def, simplified] q'
  obtain q σ μ where q: "q ∈ set Q" and match: "q ⋅ σ = ?m q'" 
    and match2: "q = ?m q' ⋅ μ" unfolding matches_iff by blast+
  let ?sm = "μ ∘⇩s σ"
  have "?m q' ⋅ Var = q ⋅ σ" unfolding match by simp
  also have "… = ?m q' ⋅ ?sm" unfolding match2 by simp
  finally have "?m q' ⋅ ?sm = ?m q' ⋅ Var" by simp
  from term_subst_eq_rev[OF this] have sigma_mu: "⋀ x. x ∈ vars_term q' ⟹ ?sm x = Var x" by auto
  show "∃q ∈ lab_lhss_all LD (set Q). matches q' q" unfolding matches_iff
  proof (rule bexI[of _ "q' ⋅ μ"], rule exI[of _ σ])
    from term_subst_eq[of q' ?sm Var, OF sigma_mu]
    show "q' ⋅ μ ⋅ σ = q'" by simp
  next
    show "q' ⋅ μ ∈ lab_lhss_all LD (set Q)"
    proof
      have "?m (q' ⋅ μ) = ?m q' ⋅ map_funs_subst ?f μ" by simp
      also have "… = ?m q' ⋅ μ"
      proof (rule term_subst_eq)
        fix x
        assume "x ∈ vars_term (?m q')"
        hence x: "x ∈ vars_term q'" by simp
        from sigma_mu[OF this] have "μ x ⋅ σ = Var x" unfolding subst_compose_def .
        then obtain y where "μ x = Var y" by (cases "μ x", auto)
        thus "map_funs_subst ?f μ x = μ x" by simp
      qed
      also have "… = q" unfolding match2 ..
      finally 
      show "?m (q' ⋅ μ) ∈ set Q" using q by simp 
    qed
  qed
qed

definition
  sem_lab_rel_tt ::
    "('f,'v)splitter ⇒ 
     ('f,'f,'l)ldecompose ⇒
     ('tp, 'f::show, 'v::show) tp_ops ⇒
     shows check ⇒ (('f,'v)rules ⇒ shows check) ⇒ 
     ('f,'v)sl_check2s ⇒
     ('f,'v)term list ⇒
     ('f,'v)rules ⇒ 
     'tp proc"
where
  "sem_lab_rel_tt splitter LD I valid check_decr check_model_lab lQ lAll tp ≡ 
    let R = tp_ops.R I tp;
        Rw = tp_ops.Rw I tp;
        nfs = tp_ops.nfs I tp;
        (lR,lRw,D) = splitter lAll (set Rw) in
    check_return ( 
      do {
        valid; 
        let Q = tp_ops.Q I tp;
        do {
          (if nfs ∧ ¬ tp_ops.Q_empty I tp then check_wf_trs D else succeed);
          check_decr D;
          check_sl_Q LD lQ Q;
          check_model_lab (set lR) R;
          check_model_lab (set lRw) Rw
        } <+? (λs. ''problem with labeled TRS:'' +#+ shows_nl +@+ s)
      })
   (tp_ops.mk I nfs lQ lR (lRw @ D))"

definition
  sem_lab_proc ::
    "('f,'f,'l)ldecompose ⇒
     ('dpp, 'f::show, 'v::show) dpp_ops ⇒
     shows check ⇒ 
     ('f,'v)sl_check1 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)sl_check2 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)rules ⇒ 
     ('f,'v)term list ⇒
     ('f,'v)rules ⇒ 
     'dpp proc"
where
  "sem_lab_proc LD I valid check_Q' check_lab check_lab' check_model_lab lPAll lQ lRAll dpp ≡ 
    let R = dpp_ops.R I dpp;
        Rw = dpp_ops.Rw I dpp;
        Pw = dpp_ops.Pw I dpp;
        P = dpp_ops.P I dpp;
        nfs = dpp_ops.nfs I dpp;
        m = dpp_ops.minimal I dpp;
        (lP,lPw,_) = model_splitter LD lPAll (set Pw);
        (lR,lRw,_) = model_splitter LD lRAll (set Rw) in
    check_return ( 
      do {
        valid; 
        let Q = dpp_ops.Q I dpp;
        do {
          check (nfs ⟶ ¬ dpp_ops.Q_empty I dpp ⟶ dpp_ops.wwf_rules I dpp) (shows ''well formedness required'');
          check_Q' lQ Q;
          check_sl_Q LD lQ Q;
          check_lab (set lP) P;
          check_lab (set lPw) Pw;
          check_model_lab (set lR) R;
          check_model_lab (set lRw) Rw;
          check_lab' lR R;
          check_lab' lRw Rw
        } <+? (λs. ''problem during labeling:'' +#+ shows_nl +@+ s)
      })
   (dpp_ops.mk I nfs m lP lPw lQ lR lRw)"

definition
  sem_lab_root_proc ::
    "('f,'f,'l)ldecompose ⇒
     ('dpp, 'f::show, 'v::show) dpp_ops ⇒
     shows check ⇒ 
     ('f,'v)sl_check1 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)sl_check2 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)rules ⇒ 
     ('f,'v)term list ⇒
     ('f,'v)rules ⇒ 
     'dpp proc"
where
  "sem_lab_root_proc LD I valid check_Q' check_lab check_lab' check_model_lab lPAll lQ lRAll dpp ≡ 
    let R = dpp_ops.R I dpp;
        Rw = dpp_ops.Rw I dpp;
        Pw = dpp_ops.Pw I dpp;
        P = dpp_ops.P I dpp;
        nfs = dpp_ops.nfs I dpp;
        m = dpp_ops.minimal I dpp;
        (lP,lPw,_) = model_splitter LD lPAll (set Pw);
        (lR,lRw,_) = model_splitter LD lRAll (set Rw) in
    check_return ( 
      do {
        valid; 
        check_allm (λ(l, r). do {
          check_no_var l;
          check_no_var r;
          check_no_defined_root (dpp_spec.is_defined I dpp) r
        }) (dpp_ops.pairs I dpp);
        check_allm (λ(l, r). check_no_var l) (dpp_ops.rules I dpp);
        let Q = dpp_ops.Q I dpp;
        do {
          check (nfs ⟶ ¬ dpp_ops.Q_empty I dpp ⟶ dpp_ops.wwf_rules I dpp) (shows ''well formedness required'');
          check_Q' lQ Q;
          check_sl_Q LD lQ Q;
          check_lab (set lP) P;
          check_lab (set lPw) Pw;
          check_model_lab (set lR) R;
          check_model_lab (set lRw) Rw;
          check_lab' lR R;
          check_lab' lRw Rw
        } <+? (λs. ''problem during labeling:'' +#+ shows_nl +@+ s)
      })
   (dpp_ops.mk I nfs m lP lPw lQ lR lRw)"

definition
  sem_lab_quasi_root_proc ::
    "('f,'f,'l)ldecompose ⇒
     ('dpp, 'f::show, 'v::show) dpp_ops ⇒
     shows check ⇒ 
     ('f,'v)sl_check0 ⇒
     ('f,'v)sl_check0 ⇒
     ('f,'v)sl_check1 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)sl_check2 ⇒
     ('f,'v)sl_check2s ⇒
     ('f,'v)rules ⇒ 
     ('f,'v)term list ⇒
     ('f,'v)rules ⇒ 
     'dpp proc"
where
  "sem_lab_quasi_root_proc LD I valid check_decr check_decr' check_lhss_more check_lab_all check_lab_all_trs check_model_lab lPAll lQ lRAll dpp ≡ 
    let R = dpp_ops.R I dpp;
        Rw = dpp_ops.Rw I dpp;
        Pw = dpp_ops.Pw I dpp;
        P = dpp_ops.P I dpp;
        nfs = dpp_ops.nfs I dpp;
        m = dpp_ops.minimal I dpp;
        (lP,lPw,_) = model_splitter LD lPAll (set Pw);
        (lR,lRw,D) = quasi_splitter LD lRAll (set Rw);
        qempty = dpp_ops.Q_empty I dpp in
    check_return ( 
      do {
        valid; 
        check (nfs ⟶ ¬ qempty ⟶ dpp_ops.wwf_rules I dpp) (shows ''well formedness required'');
        check_allm (λ(l, r). do {
          check_no_var l;
          check_no_var r;
          check_no_defined_root (dpp_spec.is_defined I dpp) r
        }) (dpp_ops.pairs I dpp);
        check_allm (λ(l, r). check_no_var l) (dpp_ops.rules I dpp);
        let Q = dpp_ops.Q I dpp;
        (if nfs ∧ ¬ qempty then check_wf_trs D else succeed);
        check_decr D;
        check_decr' D;
        check_allm (λ q. check (linear_term q) (shows ''Q must not contain non-linear terms'')) Q;
        do {
          check_lhss_more lQ Q;
          check_sl_Q LD lQ Q;
          check_lab_all (set lP) P;
          check_lab_all (set lPw) Pw;
          check_model_lab (set lR) R;
          check_model_lab (set lRw) Rw;
          check_lab_all_trs lR R;
          check_lab_all_trs lRw Rw
        } <+? (λs. ''problem during labeling:'' +#+ shows_nl +@+ s)
      })
   (dpp_ops.mk I nfs m lP lPw lQ lR (lRw @ D))"

abbreviation (input) model_lge where "model_lge ≡ λ _ _ . op ="
abbreviation (input) model_cge where "model_cge ≡ op ="

lemma decr_empty: "decr_of_ord (lge_to_lgr_rel model_lge x) y z = {}"
  unfolding decr_of_ord_def lge_to_lgr_rel_def lge_to_lgr_def Let_def by auto

locale sl_interpr_impl = 
  fixes check_Q' :: "('f :: show, 'v ::show)sl_check1"
   and  check_lab :: "('f,'v)sl_check2s"
   and  check_lab_root :: "('f,'v)sl_check2s"
   and  check_lab_root_all :: "('f,'v)sl_check2s"
   and  check_lab' :: "('f,'v)sl_check2"
   and  check_model_lab :: "('f,'v)sl_check2s"
   and  check_lab_all_trs :: "('f,'v)sl_check2"
   and  check_lab_lhss_more :: "('f :: show, 'v ::show)sl_check1"
   and  check_decr :: "('f,'v)rules ⇒ shows check"
   and  check_decr' :: "('f,'v)rules ⇒ shows check"
   and  check_valid :: "shows check"
   and  C :: "'c set"
   and  c :: "'c"
   and  I :: "('f,'c)inter"
   and  cge :: "'c ⇒ 'c ⇒ bool"
   and  lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
   and  L :: "('f,'c,'l)label"
   and  LS :: "('f,'l)labels" 
   and  LC :: "'f ⇒ nat ⇒ 'l ⇒ 'f"
   and  LD :: "'f ⇒ ('f × 'l)"
   and  L' :: "('f,'c,'l)label"
   and  LS' :: "('f,'l)labels" 
 assumes check_Q': "isOK(check_Q' lQ Q) ⟹ NF_terms (lab_lhss I L LC C (set Q)) ⊇ NF_terms (set lQ)"
   and   check_lab: "isOK(check_lab lR R) ⟹ lab_trs I L LC C (set R) ⊆ lR"
   and   check_lab_root: "isOK(check_lab_root lP P) ⟹ lab_root_trs I L L' LC C (set P) ⊆ lP"
   and   check_lab_root_all: "isOK(check_lab_root_all lP P) ⟹ lab_root_all_trs I L L' LC lge C (set P) ⊆ lP"
   and   check_lab': "⋀ lR. isOK(check_lab' lR R) ⟹ set lR ⊆ lab_trs I L LC C (set R)"
   and   check_model_lab: "isOK(check_model_lab lR R) ⟹ lab_trs I L LC C (set R) ⊆ lR ∧ qmodel I L LC C cge (set R)"
   and   check_lab_all_trs: "⋀ lR. isOK(check_lab_all_trs lR R) ⟹ set lR ⊆ sl_interpr.Lab_all_trs LC LD LS (set R)"
   and   check_lab_lhss_more: "isOK(check_lab_lhss_more lQ Q) ⟹ NF_terms (sl_interpr.Lab_lhss_more LC LD LS (set Q)) ⊇ NF_terms (set lQ)"
   and   check_decr:  "isOK(check_decr D) ⟹ decr_of_ord (lge_to_lgr_rel lge LS) LC LS ⊆ (subst.closure (set D) ∩ decr_of_ord (lge_to_lgr_rel lge LS) LC LS)^+"
   and   check_decr':  "isOK(check_decr' D) ⟹ set D ⊆ decr_of_ord (lge_to_lgr_rel lge LS) LC LS"
   and   check_valid: "isOK(check_valid) ⟹ sl_interpr_root_same C c I cge lge L LC LD LS L' LS'"
begin

lemma sem_lab_rel_tt: assumes J: "tp_spec J"
  shows "tp_spec.sound_tt_impl J (sem_lab_rel_tt splitter LD J check_valid check_decr check_model_lab lQ lAll)"
proof -
  interpret tp_spec J by fact
  show ?thesis
  proof
    fix trs trs'
    assume ok: "sem_lab_rel_tt splitter LD J check_valid check_decr check_model_lab lQ lAll trs = return trs'"
    and SN: "SN_qrel (tp_ops.qreltrs J trs')"
    let ?Q = "tp_ops.Q J trs"
    let ?R = "tp_ops.R J trs"
    let ?Rw = "tp_ops.Rw J trs"
    let ?sRw = "set ?Rw"
    let ?nfs = "NFS trs"
    obtain lR lRw D where splitter: "splitter lAll ?sRw = (lR,lRw,D)"
      by (cases "splitter lAll ?sRw", auto)
    let ?lR = "set lR"
    let ?lRw = "set lRw"
    note ok = ok[unfolded sem_lab_rel_tt_def Let_def splitter, simplified]
    from ok have valid: "isOK (check_valid)" 
      and decr: "isOK(check_decr D)"
      and Q: "isOK (check_sl_Q LD lQ ?Q)"
      and R: "isOK(check_model_lab ?lR ?R)"
      and Rw: "isOK(check_model_lab ?lRw ?Rw)"
      and wf: "?nfs ⟹ set ?Q ≠ {} ⟹ wf_trs (set D)" 
      and trs': "trs' = tp_ops.mk J ?nfs lQ lR (lRw @ D)" by auto
    from check_valid[OF valid]
    interpret sl_interpr_root_same C c I cge lge L LC LD LS L' LS' .    
    from check_model_lab[OF R] have 
      R1: "lab_trs I L LC C (set ?R) ⊆ ?lR"
      and R2: "qmodel I L LC C cge (set ?R)" by auto
    from check_model_lab[OF Rw] have 
      Rw1: "lab_trs I L LC C ?sRw ∪ set D ⊆ ?lR ∪ (?lRw ∪ set D)"
      and Rw2: "qmodel I L LC C cge ?sRw" by auto
    show "SN_qrel (tp_ops.qreltrs J trs)"
      unfolding qreltrs_sound
    proof (rule quasi_rel_SN_lab_imp_rel_SN[OF check_decr[OF decr] wf check_sl_Q[OF Q]
        SN_qrel_mono[OF subset_refl R1 Rw1] 
        R2 Rw2])
      show "SN_qrel (?nfs,set lQ, set lR, set lRw ∪ set D)"
        using SN[unfolded trs' mk_sound] by auto
    qed
  qed
qed

lemma sem_lab_proc: assumes J: "dpp_spec J"
  and L: "⋀ f. inj (L f)"
  and lge: "lge = model_lge"
  and cge: "cge = model_cge"
  shows "dpp_spec.sound_proc_impl J (sem_lab_proc LD J check_valid check_Q' check_lab check_lab' check_model_lab lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis
  proof
    fix dp dp'
    assume ok: "sem_lab_proc LD J check_valid check_Q' check_lab check_lab' check_model_lab lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    let ?Q = "dpp_ops.Q J dp"
    let ?R = "dpp_ops.R J dp"
    let ?Rw = "dpp_ops.Rw J dp"
    let ?sRw = "set ?Rw"
    let ?P = "dpp_ops.P J dp"
    let ?Pw = "dpp_ops.Pw J dp"
    let ?sPw = "set ?Pw"
    let ?nfs = "NFS dp"
    let ?m = "M dp"
    let ?splitter = "model_splitter LD"
    obtain lR lRw D where splitterR: "?splitter lRAll ?sRw = (lR,lRw,D)"
      by (cases "?splitter lRAll ?sRw", auto)
    obtain lP lPw D where splitterP: "?splitter lPAll ?sPw = (lP,lPw,D)"
      by (cases "?splitter lPAll ?sPw", auto)
    let ?lR = "set lR"
    let ?lRw = "set lRw"
    let ?lP = "set lP"
    let ?lPw = "set lPw"
    note ok = ok[unfolded sem_lab_proc_def Let_def splitterR splitterP, simplified]
    from ok have valid: "isOK (check_valid)" 
      and Q: "isOK (check_sl_Q LD lQ ?Q)"
      and Q': "isOK (check_Q' lQ ?Q)"
      and R: "isOK(check_model_lab ?lR ?R)"
      and Rw: "isOK(check_model_lab ?lRw ?Rw)"
      and R': "isOK(check_lab' lR ?R)"
      and Rw': "isOK(check_lab' lRw ?Rw)"
      and P: "isOK(check_lab ?lP ?P)"
      and Pw: "isOK(check_lab ?lPw ?Pw)"
      and wwf: "?nfs ⟹ set ?Q ≠ {} ⟹ wwf_qtrs (set ?Q) (set ?R ∪ set ?Rw)"
      and dp': "dp' = dpp_ops.mk J ?nfs ?m lP lPw lQ lR lRw" by auto
    from check_valid[OF valid]
    interpret sl_interpr_root_same C c I cge model_lge L LC LD LS L' LS' unfolding lge .
    from check_model_lab[OF R] have 
      R1: "lab_trs I L LC C (set ?R) ⊆ set lR"
      and R2: "qmodel I L LC C cge (set ?R)" by auto
    from check_model_lab[OF Rw] have 
      Rw1: "lab_trs I L LC C ?sRw ⊆ set lR ∪ set lRw"
      and Rw2: "qmodel I L LC C cge ?sRw" by auto
    show "finite_dpp (dpp_ops.dpp J dp)"
      unfolding dpp_sound      
    proof (rule sl_model_finite[OF L wwf R2 Rw2 cge decr_empty check_Q'[OF Q'] check_sl_Q[OF Q] 
        finite_dpp_mono[OF fin[unfolded dp' mk_sound] check_lab[OF P] _ refl R1]])
      show "Lab_trs (set ?P) ∪ Lab_trs (set ?Pw) ⊆ set lP ∪ set lPw"
        using check_lab[OF P] check_lab[OF Pw] by auto
      show "Lab_trs (set ?R) ∪ Lab_trs (set ?Rw) = set lR ∪ set lRw" (is "?left = ?right")
      proof
        show "?left ⊆ ?right" using R1 Rw1 by auto
        show "?right ⊆ ?left" using check_lab'[OF R'] check_lab'[OF Rw'] by auto
      qed
    qed
  qed
qed

lemma sem_lab_root_proc: assumes J: "dpp_spec J"
  and L: "⋀ f. inj (L f)"
  and lge: "lge = model_lge"
  and cge: "cge = model_cge"
  shows "dpp_spec.sound_proc_impl J (sem_lab_root_proc LD J check_valid check_Q' check_lab_root check_lab' check_model_lab lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis
  proof
    fix dp dp'
    assume ok: "sem_lab_root_proc LD J check_valid check_Q' check_lab_root check_lab' check_model_lab lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    let ?Q = "dpp_ops.Q J dp"
    let ?R = "dpp_ops.R J dp"
    let ?Rw = "dpp_ops.Rw J dp"
    let ?sRw = "set ?Rw"
    let ?P = "dpp_ops.P J dp"
    let ?Pw = "dpp_ops.Pw J dp"
    let ?sPw = "set ?Pw"
    let ?nfs = "NFS dp"
    let ?m = "M dp"
    let ?splitter = "model_splitter LD"
    obtain lR lRw D where splitterR: "?splitter lRAll ?sRw = (lR,lRw,D)"
      by (cases "?splitter lRAll ?sRw", auto)
    obtain lP lPw D where splitterP: "?splitter lPAll ?sPw = (lP,lPw,D)"
      by (cases "?splitter lPAll ?sPw", auto)
    let ?lR = "set lR"
    let ?lRw = "set lRw"
    let ?lP = "set lP"
    let ?lPw = "set lPw"
    note ok = ok[unfolded sem_lab_root_proc_def Let_def splitterR splitterP, simplified]
    from ok
    have nvar: "∀(l, r)∈ set ?P ∪ set ?Pw.
      is_Fun l ∧ is_Fun r" and ndef: "∀(l,r) ∈ set ?P ∪ set ?Pw. ¬ defined (set ?R ∪ set ?Rw) (the (root r))"
      and nvarR: "∀ (l,r) ∈ set ?R ∪ set ?Rw. is_Fun l"
      by (auto simp: split_def Let_def)
    from ok have valid: "isOK (check_valid)" 
      and Q: "isOK (check_sl_Q LD lQ ?Q)"
      and Q': "isOK (check_Q' lQ ?Q)"
      and R: "isOK(check_model_lab ?lR ?R)"
      and Rw: "isOK(check_model_lab ?lRw ?Rw)"
      and R': "isOK(check_lab' lR ?R)"
      and Rw': "isOK(check_lab' lRw ?Rw)"
      and P: "isOK(check_lab_root ?lP ?P)"
      and Pw: "isOK(check_lab_root ?lPw ?Pw)"
      and wwf: "?nfs ⟹ set ?Q ≠ {} ⟹ wwf_qtrs (set ?Q) (set ?R ∪ set ?Rw)"
      and dp': "dp' = dpp_ops.mk J ?nfs ?m lP lPw lQ lR lRw" by auto
    from check_valid[OF valid]
    interpret sl_interpr_root_same C c I cge model_lge L LC LD LS L' LS' unfolding lge .
    from check_model_lab[OF R] have 
      R1: "lab_trs I L LC C (set ?R) ⊆ set lR"
      and R2: "qmodel I L LC C cge (set ?R)" by auto
    from check_model_lab[OF Rw] have 
      Rw1: "lab_trs I L LC C (set ?Rw) ⊆ set lR ∪ set lRw"
      and Rw2: "qmodel I L LC C cge (set ?Rw)" by auto
    show "finite_dpp (dpp_ops.dpp J dp)"
      unfolding dpp_sound      
    proof (rule sl_model_root_finite[OF L wwf R2 Rw2 cge decr_empty decr_empty check_Q'[OF Q'] check_sl_Q[OF Q] nvar]) 
      show "finite_dpp (?nfs,?m,Lab_root_trs (set ?P), Lab_root_trs (set ?Pw), set lQ, Lab_trs (set ?R), Lab_trs (set ?Rw))" 
      proof (rule finite_dpp_mono[OF fin[unfolded dp' mk_sound] check_lab_root[OF P] _ refl R1])
        show "Lab_root_trs (set ?P) ∪ Lab_root_trs ?sPw ⊆ set lP ∪ set lPw"
          using check_lab_root[OF P] check_lab_root[OF Pw] by auto
        show "Lab_trs (set ?R) ∪ Lab_trs ?sRw = set lR ∪ set lRw" (is "?left = ?right")
        proof
          show "?left ⊆ ?right" using R1 Rw1 by auto
          show "?right ⊆ ?left" using check_lab'[OF R'] check_lab'[OF Rw'] by auto
        qed
      qed
    next
      show "∀ (s,t) ∈ set ?P ∪ set ?Pw. ¬ defined (applicable_rules (set ?Q) (set ?R ∪ set ?Rw)) (the (root t))"
        using ndef_applicable_rules ndef by blast
    qed (insert nvarR, auto)
  qed
qed

lemma sem_lab_quasi_root_proc: assumes J: "dpp_spec J"
  shows "dpp_spec.sound_proc_impl J (sem_lab_quasi_root_proc LD J check_valid check_decr check_decr' check_lab_lhss_more 
    check_lab_root_all check_lab_all_trs check_model_lab lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis
  proof
    fix dp dp'
    assume ok: "sem_lab_quasi_root_proc LD J check_valid check_decr check_decr' check_lab_lhss_more check_lab_root_all check_lab_all_trs check_model_lab lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    let ?Q = "dpp_ops.Q J dp"
    let ?R = "dpp_ops.R J dp"
    let ?Rw = "dpp_ops.Rw J dp"
    let ?sRw = "set ?Rw"
    let ?P = "dpp_ops.P J dp"
    let ?Pw = "dpp_ops.Pw J dp"
    let ?sPw = "set ?Pw"
    let ?nfs = "NFS dp"
    let ?m = "M dp"
    let ?msplitter = "model_splitter LD"
    let ?qsplitter = "quasi_splitter LD"
    obtain lR lRw D where splitterR: "?qsplitter lRAll ?sRw = (lR,lRw,D)"
      by (cases "?qsplitter lRAll ?sRw", auto)
    obtain lP lPw D' where splitterP: "?msplitter lPAll ?sPw = (lP,lPw,D')"
      by (cases "?msplitter lPAll ?sPw", auto)
    let ?lR = "set lR"
    let ?lRw = "set lRw"
    let ?lP = "set lP"
    let ?lPw = "set lPw"
    note ok = ok[unfolded sem_lab_quasi_root_proc_def Let_def splitterR splitterP, simplified]
    from ok
    have nvar: "∀(l, r)∈ set ?P ∪ set ?Pw.
      is_Fun l ∧ is_Fun r" and ndef: "∀(l,r) ∈ set ?P ∪ set ?Pw. ¬ defined (set ?R ∪ set ?Rw) (the (root r))"
      and nvarR: "∀ (l,r) ∈ set ?R ∪ set ?Rw. is_Fun l"
      by (auto simp: split_def Let_def)
    from ok have valid: "isOK (check_valid)" 
      and Q: "isOK (check_sl_Q LD lQ ?Q)"
      and Q': "isOK (check_lab_lhss_more lQ ?Q)"
      and lQ: "⋀ q. q ∈ set ?Q ⟹ linear_term q"
      and D: "isOK(check_decr D)"
      and D': "isOK(check_decr' D)"
      and R: "isOK(check_model_lab ?lR ?R)"
      and Rw: "isOK(check_model_lab ?lRw ?Rw)"
      and R': "isOK(check_lab_all_trs lR ?R)"
      and Rw': "isOK(check_lab_all_trs lRw ?Rw)"
      and P: "isOK(check_lab_root_all ?lP ?P)"
      and Pw: "isOK(check_lab_root_all ?lPw ?Pw)"
      and wf: "?nfs ⟹ set ?Q ≠ {} ⟹ wf_trs (set D)" 
      and wwf: "?nfs ⟹  set ?Q ≠ {} ⟹ wwf_qtrs (set ?Q) (set ?R ∪ set ?Rw)"
      and dp': "dp' = dpp_ops.mk J ?nfs ?m lP lPw lQ lR (lRw @ D)" by auto
    from check_valid[OF valid]
    interpret sl_interpr_root_same C c I cge lge L LC LD LS L' LS' .
    from check_model_lab[OF R] have 
      R1: "lab_trs I L LC C (set ?R) ⊆ set lR"
      and R2: "qmodel I L LC C cge (set ?R)" by auto
    from check_model_lab[OF Rw] have 
      Rw1: "lab_trs I L LC C (set ?Rw) ⊆ set lR ∪ set lRw"
      and Rw2: "qmodel I L LC C cge (set ?Rw)" by auto
    show "finite_dpp (dpp_ops.dpp J dp)"
      unfolding dpp_sound      
    proof (rule sl_qmodel_root_finite[OF R2 Rw2 check_decr[OF D] wf wwf check_decr'[OF D'] check_lab_lhss_more[OF Q']
          check_sl_Q[OF Q] lQ R1 Rw1 _ nvar])
      show "set lR ∪ set lRw ⊆ Lab_all_trs (set ?R ∪ set ?Rw)"
        using check_lab_all_trs[OF R'] check_lab_all_trs[OF Rw'] unfolding Lab_all_trs_def by auto
      show "∀ (s,t) ∈ set ?P ∪ set ?Pw. ¬ defined (applicable_rules (set ?Q) (set ?R ∪ set ?Rw)) (the (root t))"
        using ndef_applicable_rules ndef by blast
      show "finite_dpp (?nfs,?m,Lab_root_all_trs (set ?P), Lab_root_all_trs (set ?Pw), set lQ, set lR, set lRw ∪ set D)"
      proof (rule finite_dpp_mono[OF fin[unfolded dp' mk_sound] check_lab_root_all[OF P] _ refl subset_refl])
        show "Lab_root_all_trs (set ?P) ∪ Lab_root_all_trs (set ?Pw) ⊆ set lP ∪ set lPw"
          using check_lab_root_all[OF P]  check_lab_root_all[OF Pw]  by auto
      qed simp
    qed (insert nvarR, auto)
  qed
qed

lemma check_decr_rstep: assumes check: "isOK(check_decr lR)" shows "decr_of_ord (lge_to_lgr_rel lge LS) LC LS ⊆ (rstep (set lR))^+"
proof -
  show ?thesis unfolding rstep_ctxt_closure_subst_closure 
    by (rule subset_trans[OF check_decr[OF check]], rule trancl_mono_set,
    rule subset_trans[OF _ ctxt.subset_closure], auto)
qed
end

subsection ‹checking the various model / ... conditions›

fun
  check_sl_rule_ass ::
    "bool ⇒ ('f::show,'c::show)inter ⇒ ('f,'c,'l)label
     ⇒ ('f,'l,'lf :: show)lcompose 
     ⇒ ('c ⇒ 'c ⇒ bool)
     ⇒ ('lf,'v)trs
     ⇒ ('v::show,'c)assign ⇒ ('f,'v)rule ⇒ shows check"
where
  "check_sl_rule_ass mc I L LC cge lR α (l, r) = do {
     let cl_ll = eval_lab I L LC α l;
     let cr_lr = eval_lab I L LC α r;
     check (mc ⟶ (cge (fst cl_ll) (fst cr_lr)))
       (''rule '' +#+ shows_rule (l, r) +@+ '' violates the model condition, [lhs] = ''
         +#+ shows (fst cl_ll) +@+ '', [rhs] = '' +#+ shows (fst cr_lr));
     check ((snd cl_ll, snd cr_lr) ∈ lR)
       (''labeled rule '' +#+ shows_rule (snd cl_ll, snd cr_lr) +@+ shows_string '' missing'')
   }"

fun
  lab_rule_ass ::
    "('f,'c)inter ⇒ ('f,'c,'l)label
     ⇒ ('f,'l,'lf)lcompose 
     ⇒ ('v,'c)assign ⇒ ('f,'v)rule ⇒ ('lf,'v)rule"
where
  "lab_rule_ass I L LC α rule = 
     (lab I L LC α (fst rule), lab I L LC α (snd rule))"

fun
  check_sl_rule_all_ass ::
    "('f::show,'c::show)inter ⇒ ('f,'c,'l)label ⇒ ('f,'c,'l)label
     ⇒ ('f,'l,'lf :: show)lcompose 
     ⇒ ('l ⇒ 'l list)
     ⇒ ('lf,'v)trs
     ⇒ ('v::show,'c)assign ⇒ ('f,'v)rule ⇒ shows check"
where
  "check_sl_rule_all_ass I L L' LC gen_smaller lR α (l, Fun f ts) = do {
     let ll = lab_root I L L' LC α l;
         clts = map (eval_lab I L LC α) ts;
         lts = map snd clts;
         l'   = L' f (map fst clts);
         n = length ts;
         small = gen_smaller l' in
     check_allm (λ l'. check ((ll, Fun (LC f n l') lts) ∈ lR) 
       (''labeled rule '' +#+ shows_rule (ll, Fun (LC f n l') lts) +@+ shows_string '' missing'')) small
   }" |
  "check_sl_rule_all_ass I L L' LC gen_smaller lR α (l, Var x) = do {
     let ll = lab_root I L L' LC α l;
     let lr = lab_root I L L' LC α (Var x) in
   check ((ll, lr) ∈ lR) 
       (''labeled rule '' +#+ shows_rule (ll, lr) +@+ shows_string '' missing'')
   }"

fun
  check_sl_rule_root ::
    "('f::show,'c::show)inter ⇒ ('f,'c,'l)label ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf :: show)lcompose 
     ⇒ 'c list 
     ⇒ ('lf :: show,'v)trs ⇒ ('f,'v::show)rule ⇒ shows check"
where
  "check_sl_rule_root I L L' LC C lR lr = check_allm (λα. 
  let la = lab_root I L L' LC α;
      l =  la (fst lr);
      r =  la (snd lr)
    in check ((l,r) ∈ lR) (shows ''labeled rule '' +@+ shows_rule (l,r) +@+ shows '' is missing''))
     (map fun_of (enum_vectors C (vars_rule_impl lr)))"

fun
  check_sl_rule ::
    "('f::show,'c::show)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf :: show)lcompose 
     ⇒ 'c list 
     ⇒ ('c ⇒ 'c ⇒ bool)
     ⇒ bool
     ⇒ ('lf :: show,'v)trs ⇒ ('f,'v::show)rule ⇒ shows check"
where
  "check_sl_rule I L LC C cge mc lR lr = check_allm (λα. check_sl_rule_ass mc I L LC cge lR α lr) 
     (map fun_of (enum_vectors C (vars_rule_impl lr)))"

fun
  check_sl_rule_all ::
    "('f::show,'c::show)inter ⇒ ('f,'c,'l)label ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf :: show)lcompose 
     ⇒ 'c list 
     ⇒ ('l ⇒ 'l list)
     ⇒ ('lf :: show,'v)trs ⇒ ('f,'v::show)rule ⇒ shows check"
where
  "check_sl_rule_all I L L' LC C gen_smaller lR lr = check_allm (λα. check_sl_rule_all_ass I L L' LC gen_smaller lR α lr) 
     (map fun_of (enum_vectors C (vars_rule_impl lr)))"

lemma check_sl_rule_sound[simp]:
  fixes lR :: "('f::show,'v::show)trs" and I :: "('f,'c::show)inter" 
  assumes "isOK (check_sl_rule I L LC C cge mc lR (l,r))"
  shows "(mc ⟶ qmodel_rule I L LC (set C) cge l r) ∧ lab_rule I L LC (set C) (l,r) ⊆ lR"
proof (cases C)
  case Nil
  thus ?thesis unfolding lab_rule_def wf_assign_def by auto
next
  case (Cons c D)
  let ?C = "Cons c D"
  let ?V = "vars_rule_impl (l,r) :: 'v list"
  from assms Cons have check: "∀ α ∈ set (map fun_of (enum_vectors ?C ?V)). isOK(check_sl_rule_ass mc I L LC cge lR α (l,r))"
    by auto
  have "∀ α. wf_assign (set ?C) α ⟶ isOK(check_sl_rule_ass mc I L LC cge lR α (l,r))"
  proof (intro allI, intro impI)
    fix α :: "'v ⇒ 'c"
    assume wf_ass: "wf_assign (set ?C) α"
    from enum_vectors_complete obtain vec where vec: "vec ∈ set (enum_vectors ?C ?V) ∧ (∀ x ∈ set ?V. ∀ c ∈ set ?C. α x = c ⟶ fun_of vec x = c)"
      by best
    let ?β = "fun_of vec"
    from wf_ass vec have "∀ x ∈ set ?V. α x = ?β x" unfolding wf_assign_def by auto
    hence l: "(∀ x ∈ vars_term l. ?β x = α x)" and r: "(∀ x ∈ vars_term r. ?β x = α x) " 
      unfolding set_vars_rule_impl vars_rule_def by auto
    have equal: "eval_lab I L LC α l = eval_lab I L LC ?β l ∧ eval_lab I L LC α r = eval_lab I L LC ?β r" 
      unfolding eval_lab_independent[OF l] eval_lab_independent[OF r] by auto
    from vec check have "isOK(check_sl_rule_ass mc I L LC cge lR ?β (l,r))" by auto
    with equal show "isOK(check_sl_rule_ass mc I L LC cge lR α (l,r))" by auto
  qed
  thus ?thesis using Cons unfolding lab_rule_def by (auto simp: Let_def)
qed

declare check_sl_rule.simps[simp del]

lemma check_sl_rule_root:
  fixes lR :: "('f::show,'v::show)trs" and I :: "('f,'c::show)inter" 
  assumes "isOK (check_sl_rule_root I L L' LC C lR (l,r))"
  shows "lab_root_rule I L L' LC (set C) (l,r) ⊆ lR"
proof (cases C)
  case Nil
  thus ?thesis unfolding lab_root_rule_def wf_assign_def by auto
next
  case (Cons c D)
  let ?C = "Cons c D"
  let ?V = "vars_rule_impl (l,r) :: 'v list"
  let ?L = "lab_root I L L' LC"
  from assms Cons have check: "∀ α ∈ set (map fun_of (enum_vectors ?C ?V)). (?L α l, ?L α r) ∈ lR"
    by (auto simp: Let_def)
  show ?thesis unfolding lab_root_rule_def fst_conv snd_conv 
  proof (clarify)
    fix x y :: "('f,'v)term" and α :: "('v,'c)assign"
    assume wf_ass: "wf_assign (set C) α"
    from enum_vectors_complete obtain vec where vec: "vec ∈ set (enum_vectors ?C ?V) ∧ (∀ x ∈ set ?V. ∀ c ∈ set ?C. α x = c ⟶ fun_of vec x = c)"
      by best
    let ?β = "fun_of vec"
    from wf_ass vec have "∀ x ∈ set ?V. α x = ?β x" unfolding wf_assign_def Cons by auto
    hence l: "(∀ x ∈ vars_term l. ?β x = α x)" and r: "(∀ x ∈ vars_term r. ?β x = α x) " 
      unfolding set_vars_rule_impl vars_rule_def by auto
    have equal: "?L α l = ?L ?β l ∧ ?L α r = ?L ?β r" 
      unfolding lab_root_independent[OF l] lab_root_independent[OF r] by auto
    from vec check equal
    show "(?L α l, ?L α r) ∈ lR" by auto
  qed
qed

declare check_sl_rule_root.simps[simp del]

fun
  lab_rule_list ::
    "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf)lcompose 
     ⇒ 'c list 
     ⇒ ('f,'v)rule ⇒ ('lf,'v)rules"
where
  "lab_rule_list I L LC C lr = map (λα. lab_rule_ass I L LC α lr) 
     (map fun_of (enum_vectors C (vars_rule_impl lr)))"

lemma lab_rule_list:
  fixes L :: "('f,'c,'l)label" and  I :: "('f,'c)inter" 
  and rule :: "('f,'v)rule"
  assumes C: "C ≠ []"
  shows "set (lab_rule_list I L LC C rule) = lab_rule I L LC (set C) rule" (is "?list = ?set")
proof -
  obtain l r where rule: "rule = (l,r)" by force
  let ?V = "vars_rule_impl rule"
  let ?lab = "lab I L LC"
  let ?lab_rule = "λ α. (?lab α (fst rule), ?lab α (snd rule))"
  {
    fix α :: "'v ⇒ 'c"
    assume wf_ass: "wf_assign (set C) α"
    from enum_vectors_complete[OF C] obtain vec where vec: "vec ∈ set (enum_vectors C ?V) ∧ (∀ x ∈ set ?V. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c)"
      by best
    let ?β = "fun_of vec"
    from wf_ass vec have "∀ x ∈ set ?V. α x = ?β x" unfolding wf_assign_def by auto
    hence l: "(∀ x ∈ vars_term l. ?β x = α x)" and r: "(∀ x ∈ vars_term r. ?β x = α x)" 
      unfolding rule set_vars_rule_impl vars_rule_def by auto
    have equal: "?lab α l = ?lab ?β l" "?lab α r = ?lab ?β r" 
      unfolding eval_lab_independent[OF l] eval_lab_independent[OF r] by auto
    hence "?lab_rule α ∈ ?list" unfolding rule fst_conv snd_conv equal
      using vec unfolding lab_rule_list.simps rule by auto
  }
  hence one: "?set ⊆ ?list" unfolding lab_rule_def by auto
  {
    fix vec
    assume vec: "vec ∈ set (enum_vectors C ?V)"
    let ?β = "fun_of vec"
    let ?α = "λ x. if (x ∈ set ?V) then ?β x else hd C"
    have "wf_assign (set C) ?α"
      unfolding wf_assign_def
    proof (clarify)
      fix x
      show "?α x ∈ set C"
      proof (cases "x ∈ set ?V")
        case False
        thus ?thesis using C by auto
      next
        case True
        with enum_vectors_sound[OF True vec]
        show ?thesis by auto
      qed
    qed
    hence mem: "(?lab ?α l, ?lab ?α r) ∈ ?set"
      unfolding rule lab_rule_def by auto
    have "∀ x ∈ set ?V. ?α x = ?β x" by auto
    hence l: "(∀ x ∈ vars_term l. ?β x = ?α x)" and r: "(∀ x ∈ vars_term r. ?β x = ?α x)" 
      unfolding rule set_vars_rule_impl vars_rule_def by auto
    have equal: "?lab ?α l = ?lab ?β l" "?lab ?α r = ?lab ?β r" 
      unfolding eval_lab_independent[OF l] eval_lab_independent[OF r] by auto
    from mem[unfolded equal]
    have "(?lab ?β (fst rule), ?lab ?β (snd rule)) ∈ ?set" unfolding rule by auto
  }
  hence "?list ⊆ ?set" by auto
  with one show ?thesis by auto
qed
   
declare lab_rule_list.simps[simp del]

definition  lab_trs_list ::
    "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf)lcompose 
     ⇒ 'c list 
     ⇒ ('f,'v)rules ⇒ ('lf,'v)rules"
where
  "lab_trs_list I L LC C R = concat (map (lab_rule_list I L LC C) R)"

lemma lab_trs_list:
  fixes L :: "('f,'c,'l)label" and  I :: "('f,'c)inter" 
  and R :: "('f,'v)rules"
  assumes C: "C ≠ []"
  shows "set (lab_trs_list I L LC C R) = lab_trs I L LC (set C) (set R)"
  unfolding lab_trs_list_def using lab_rule_list[OF C, of I L LC]
  by auto

fun
  lab_lhs_list ::
    "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf)lcompose 
     ⇒ 'c list 
     ⇒ ('f,'v)term ⇒ ('lf,'v)term list"
where
  "lab_lhs_list I L LC C t = map (λα. lab I L LC α t) 
     (map fun_of (enum_vectors C (vars_term_impl t)))"

lemma lab_lhs_list:
  fixes L :: "('f,'c,'l)label" and  I :: "('f,'c)inter" 
  and t :: "('f,'v)term"
  assumes C: "C ≠ []"
  shows "set (lab_lhs_list I L LC C t) = lab_lhs I L LC (set C) t" (is "?list = ?set")
proof -
  let ?V = "vars_term_impl t"
  let ?lab = "lab I L LC"
  let ?lab_lhs = "λ α. ?lab α t"
  {
    fix α :: "'v ⇒ 'c"
    assume wf_ass: "wf_assign (set C) α"
    from enum_vectors_complete[OF C] obtain vec where vec: "vec ∈ set (enum_vectors C ?V) ∧ (∀ x ∈ set ?V. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c)"
      by best
    let ?β = "fun_of vec"
    from wf_ass vec have "∀ x ∈ set ?V. α x = ?β x" unfolding wf_assign_def by auto
    hence t: "(∀ x ∈ vars_term t. ?β x = α x)" by auto 
    have equal: "?lab α t = ?lab ?β t" 
      unfolding eval_lab_independent[OF t] by auto
    hence "?lab_lhs α ∈ ?list" unfolding equal
      using vec by auto
  }
  hence one: "?set ⊆ ?list" unfolding lab_lhs_def by auto
  {
    fix vec
    assume vec: "vec ∈ set (enum_vectors C ?V)"
    let ?β = "fun_of vec"
    let ?α = "λ x. if (x ∈ set ?V) then ?β x else hd C"
    have "wf_assign (set C) ?α"
      unfolding wf_assign_def
    proof (clarify)
      fix x
      show "?α x ∈ set C"
      proof (cases "x ∈ set ?V")
        case False
        thus ?thesis using C by auto
      next
        case True
        with enum_vectors_sound[OF True vec]
        show ?thesis by auto
      qed
    qed
    hence mem: "?lab_lhs ?α ∈ ?set"
      unfolding lab_lhs_def by auto
    have "∀ x ∈ set ?V. ?α x = ?β x" by auto
    hence t: "(∀ x ∈ vars_term t. ?β x = ?α x)"
      by auto
    have equal: "?lab_lhs ?α = ?lab_lhs ?β"
      unfolding eval_lab_independent[OF t] by auto
    from mem[unfolded equal]
    have "?lab_lhs ?β ∈ ?set" by auto
  }
  hence "?list ⊆ ?set" by auto
  with one show ?thesis by auto
qed
   
declare lab_lhs_list.simps[simp del]

definition lab_lhss_list ::
    "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'lf)lcompose 
     ⇒ 'c list 
     ⇒ ('f,'v)term list ⇒ ('lf,'v)term list"
where
  "lab_lhss_list I L LC C Q = concat (map (lab_lhs_list I L LC C) Q)"

lemma lab_lhss_list:
  fixes L :: "('f,'c,'l)label" and  I :: "('f,'c)inter" 
  and Q :: "('f,'v)term list"
  assumes C: "C ≠ []"
  shows "set (lab_lhss_list I L LC C Q) = lab_lhss I L LC (set C) (set Q)"
  unfolding lab_lhss_list_def using lab_lhs_list[OF C, of I L LC]
  by auto

definition check_sl_Q' :: "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'f)lcompose 
     ⇒ 'c list ⇒ ('f :: show,'v :: show)term list ⇒ ('f,'v)term list ⇒ shows check"
  where "check_sl_Q' I L LC C lQ Q ≡ do {
  check (C ≠ []) (shows ''carrier must be non-empty'');
  check_NF_vars_subset (lab_lhss_list I L LC C Q) lQ
    <+? (λ l. shows ''labeled term '' +@+ shows_term l +@+ shows '' is missing'')
  }"

lemma check_sl_Q': assumes ok: "isOK(check_sl_Q' I L LC C lQ Q)"
  shows "NF_terms (lab_lhss I L LC (set C) (set Q)) ⊇ NF_terms (set lQ)"
proof -
  note ok = ok[unfolded check_sl_Q'_def]
  from ok have "C ≠ []" by auto
  from ok lab_lhss_list[OF this, of I L LC Q]
  show ?thesis 
    by (intro NF_vars_subset, auto)
qed

definition check_sl_lab' :: "('f,'c)inter ⇒ ('f,'c,'l)label 
     ⇒ ('f,'l,'f)lcompose 
     ⇒ 'c list ⇒ ('f :: show,'v :: show)rules ⇒ ('f,'v)rules ⇒ shows check"
  where "check_sl_lab' I L LC C lR R ≡ do {
  check (C ≠ []) (shows ''carrier must be non-empty'');
  check_subseteq lR (lab_trs_list I L LC C R)
    <+? (λ lr. shows ''labeled rule '' +@+ shows_rule lr +@+ shows '' is not allowed'')
  }"

lemma check_sl_lab': assumes ok: "isOK(check_sl_lab' I L LC C lR R)"
  shows "set lR ⊆ lab_trs I L LC (set C) (set R)"
proof -
  note ok = ok[unfolded check_sl_lab'_def]
  from ok have "C ≠ []" by auto
  from ok lab_trs_list[OF this, of I L LC R]
  show ?thesis by auto
qed

lemma check_sl_rule_all_sound:
  fixes lR :: "('f::show,'v::show)trs" and I :: "('f,'c::show)inter" 
  assumes ok: "isOK (check_sl_rule_all I L L' LC C gen_smaller lR (l,r))"
  and gen: "⋀ f n l l'. lge f n l l' ⟹ l' ∈ set (gen_smaller l)"
  shows "lab_root_all_rule I L L' LC lge (set C) (l,r) ⊆ lR"
proof (cases C)
  case Nil
  thus ?thesis unfolding lab_root_all_rule_def wf_assign_def by auto
next
  case (Cons c D)
  let ?C = "Cons c D"
  let ?V = "vars_rule_impl (l,r) :: 'v list"
  from assms Cons have check: "∀ α ∈ set (map fun_of (enum_vectors ?C ?V)). isOK(check_sl_rule_all_ass I L L' LC gen_smaller lR α (l,r))"
    by auto
  have check: "∀ α. wf_assign (set ?C) α ⟶ isOK(check_sl_rule_all_ass I L L' LC gen_smaller lR α (l,r))"
  proof (intro allI, intro impI)
    fix α :: "'v ⇒ 'c"
    assume wf_ass: "wf_assign (set ?C) α"
    from enum_vectors_complete obtain vec where vec: "vec ∈ set (enum_vectors ?C ?V) ∧ (∀ x ∈ set ?V. ∀ c ∈ set ?C. α x = c ⟶ fun_of vec x = c)"
      by best
    let ?β = "fun_of vec"
    from wf_ass vec have "∀ x ∈ set ?V. α x = ?β x" unfolding wf_assign_def by auto
    hence l: "(∀ x ∈ vars_term l. ?β x = α x)" and r: "(∀ x ∈ vars_term r. ?β x = α x) " 
      unfolding set_vars_rule_impl vars_rule_def by auto
    have equal: "lab_root I L L' LC α l = lab_root I L L' LC ?β l ∧ lab_root I L L' LC α r = lab_root I L L' LC ?β r" 
      unfolding lab_root_independent[OF l] lab_root_independent[OF r] by auto
    from vec check have check: "isOK(check_sl_rule_all_ass I L L' LC gen_smaller lR ?β (l,r))" by auto
    show "isOK(check_sl_rule_all_ass I L L' LC gen_smaller lR α (l,r))" 
    proof (cases r)
      case (Var x)
      with equal check show ?thesis by simp
    next
      case (Fun f ts)
      with r have "⋀ t. t ∈ set ts ⟹ ∀ x ∈ vars_term t. ?β x = α x" by auto
      from eval_lab_independent[OF this, of _ I L LC] 
      have map: "map (eval_lab I L LC α) ts = map (eval_lab I L LC ?β) ts" by auto
      from equal[THEN conjunct1] check
      show ?thesis unfolding Fun
        by (simp add: Let_def map)
    qed
  qed
  note check = check[unfolded Cons[symmetric], THEN spec, THEN mp]
  { 
    fix α lr
    assume wf: "wf_assign (set C) α" and lr: "lr ∈ lab_root_all I L L' LC lge α r"
    note ok = check[OF wf]
    have "(lab_root I L L' LC α l, lr) ∈ lR" 
    proof (cases r)
      case (Var x)
      with ok lr show ?thesis by (simp add: Let_def)
    next
      case (Fun f ts)
      let ?n = "length ts"
      from lr[unfolded Fun]
      obtain l' where lr: "lr = Fun (LC f ?n l') (map (lab I L LC α) ts)" and lge: "lge f ?n (L' f (map (eval I L LC α) ts)) l'" 
        by (auto simp: o_def)
      from gen[OF lge] have l': "l' ∈ set (gen_smaller (L' f (map (eval I L LC α) ts)))" by simp
      from ok[unfolded Fun] l' show ?thesis
        unfolding lr by (auto simp: Let_def o_def)
    qed
  }
  thus ?thesis unfolding lab_root_all_rule_def by auto 
qed

declare check_sl_rule_all.simps[simp del]

type_synonym ('f,'c,'l,'v)sl_check4 =
  "('f,'c)inter ⇒ ('f,'c,'l)label ⇒ 'c list ⇒ ('c ⇒ 'c ⇒ bool) ⇒ ('f ⇒ nat ⇒ 'l ⇒ 'f) ⇒ ('f,'v)rules ⇒ ('f,'v)rules
   ⇒ shows check"

type_synonym ('f,'c,'l,'v)sl_check4_set =
  "('f,'c)inter ⇒ ('f,'c,'l)label ⇒ 'c list ⇒ ('c ⇒ 'c ⇒ bool) ⇒ ('f ⇒ nat ⇒ 'l ⇒ 'f) ⇒ ('f,'v)trs ⇒ ('f,'v)rules
   ⇒ shows check"

definition
  check_sl_model_lab_trs_set  :: "('f::show,'c::show,'l,'v::show)sl_check4_set" 
where
  "check_sl_model_lab_trs_set I L C cge labl lR R ≡ check_allm (check_sl_rule I L labl C cge True lR) R"

definition
  check_sl_model_lab_trs :: "('f::show,'c::show,'l,'v::show)sl_check4_set" 
where
  "check_sl_model_lab_trs I L C cge labl lR R ≡ check_sl_model_lab_trs_set I L C cge labl lR R"

definition 
  check_sl_lab_trs_set :: "('f::show,'c::show,'l,'v::show)sl_check4_set" 
where
  "check_sl_lab_trs_set I L C cge labl lP P ≡ check_allm (check_sl_rule I L labl C cge False lP) P"

definition 
  check_sl_lab_trs :: "('f::show,'c::show,'l,'v::show)sl_check4_set" 
where
  "check_sl_lab_trs I L C cge labl lP P ≡ check_sl_lab_trs_set I L C cge labl lP P"

definition 
  check_sl_lab_root_trs 
where
  "check_sl_lab_root_trs I L L' C labl lP P ≡ check_allm (check_sl_rule_root I L L' labl C lP) P"

lemma check_sl_lab_trs_set_sound:
  assumes "isOK(check_sl_lab_trs_set I L C cge labl lP P)"
  shows "lab_trs I L labl (set C) (set P) ⊆ lP"
proof -
  from assms have check: "∀ (l,r) ∈ set P. isOK(check_sl_rule I L labl C cge False lP (l,r))"
    unfolding check_sl_lab_trs_set_def by auto
  have "∀ (l,r) ∈ set P. lab_rule I L labl (set C) (l,r) ⊆ lP" 
  proof (clarify)
    fix l r ll lr
    assume lr: "(l,r) ∈ set P" and llr: "(ll,lr) ∈ lab_rule I L labl (set C) (l,r)"
    from lr check have "isOK(check_sl_rule I L labl C cge False lP (l,r))" by auto 
    hence "lab_rule I L labl (set C) (l,r) ⊆ lP" by auto
    with lr llr show "(ll,lr) ∈ lP" by auto
  qed
  thus ?thesis by auto
qed

lemma check_sl_lab_trs_sound:
  "isOK(check_sl_lab_trs I L C cge labl lP P) ⟹ lab_trs I L labl (set C) (set P) ⊆ lP"
  using check_sl_lab_trs_set_sound unfolding check_sl_lab_trs_def .


lemma check_sl_model_lab_trs_set_sound: 
  fixes label :: "('f :: show ⇒ nat ⇒ 'l ⇒ 'f)"
    and R :: "('f :: show, 'v :: show)rules"
  assumes "isOK(check_sl_model_lab_trs_set I L C cge label lR R)"
  shows "lab_trs I L label (set C) (set R) ⊆ lR ∧ qmodel I L label (set C) cge (set R)"
proof -
  from assms have check: "∀ (l,r) ∈ set R. isOK(check_sl_rule I L label C cge True lR (l,r))"
    unfolding check_sl_model_lab_trs_set_def by auto
  have "∀ (l,r) ∈ set R. qmodel_rule I L label (set C) cge l r ∧ lab_rule I L label (set C) (l,r) ⊆ lR" 
  proof (clarify)
    fix l r
    assume lr: "(l,r) ∈ set R" 
    from lr check have "isOK(check_sl_rule I L label C cge True lR (l,r))" by auto 
    thus "qmodel_rule I L label (set C) cge l r ∧ lab_rule I L label (set C) (l,r) ⊆ lR" by auto
  qed
  thus ?thesis unfolding qmodel_def by auto
qed

lemma check_sl_model_lab_trs_sound: 
  "isOK(check_sl_model_lab_trs I L C cge labl lR R) ⟹ lab_trs I L labl (set C) (set R) ⊆ lR ∧ qmodel I L labl (set C) cge (set R)"
  using check_sl_model_lab_trs_set_sound unfolding check_sl_model_lab_trs_def .
  

lemma check_sl_lab_root_trs_sound: fixes lP :: "('f :: show, 'v :: show)trs" and P :: "('f,'v)rules"
  and I :: "('f,'c::show)inter" 
  assumes "isOK(check_sl_lab_root_trs I L L' C labl lP P)"
  shows "lab_root_trs I L L' labl (set C) (set P) ⊆ lP"
proof -
  from assms have check: "∀ (l,r) ∈ set P. isOK(check_sl_rule_root I L L' labl C lP (l,r))"
    unfolding check_sl_lab_root_trs_def by auto
  have "∀ (l,r) ∈ set P. lab_root_rule I L L' labl (set C) (l,r) ⊆ lP" 
  proof (clarify)
    fix l r ll lr :: "('f,'v)term"
    assume lr: "(l,r) ∈ set P" and llr: "(ll,lr) ∈ lab_root_rule I L L' labl (set C) (l,r)"
    from lr check have check: "isOK(check_sl_rule_root I L L' labl C lP (l,r))" by auto 
    from check_sl_rule_root[OF check]
    have"lab_root_rule I L L' labl (set C) (l,r) ⊆ lP" .
    with lr llr show "(ll,lr) ∈ lP" by auto
  qed
  thus ?thesis by auto
qed

definition 
  check_sl_lab_all_trs 
where
  "check_sl_lab_all_trs I L L' C gen labl lP P ≡ check_allm (check_sl_rule_all I L L' labl C gen lP) P"


lemma check_sl_lab_all_trs_sound: 
  fixes label :: "('f :: show ⇒ nat ⇒ 'l ⇒ 'f)"
    and P :: "('f :: show, 'v :: show)rules"
  assumes ok: "isOK(check_sl_lab_all_trs I L L' C gen label lP P)"
  and gen: "⋀ f n l l'. lge f n l l' ⟹ l' ∈ set (gen l)"
  shows "lab_root_all_trs I L L' label lge (set C) (set P) ⊆ lP"
proof -
  from ok have check: "∀ (l,r) ∈ set P. isOK(check_sl_rule_all I L L' label C gen lP (l,r))"
    unfolding check_sl_lab_all_trs_def by auto
  have "∀ (l,r) ∈ set P. lab_root_all_rule I L L' label lge (set C) (l,r) ⊆ lP" 
  proof (clarify)
    fix l r ll lr
    assume lr: "(l,r) ∈ set P" and llr: "(ll,lr) ∈ lab_root_all_rule I L L' label lge (set C) (l,r)"
    from lr check have "isOK(check_sl_rule_all I L L' label C gen lP (l,r))" by auto 
    from check_sl_rule_all_sound[OF this gen]
    have "lab_root_all_rule I L L' label lge (set C) (l,r) ⊆ lP" by simp
    with lr llr show "(ll,lr) ∈ lP" by auto
  qed
  thus ?thesis by auto
qed

lemma (in sl_interpr) Lab_lhss_more_instance_term: 
  "Lab_lhss_more Q = { l. ∃ q. q ∈ Q ∧ instance_term l (map_funs_term_wa (λ (f,n). {g. (g,n) ∈ F_all ∧ UNLAB g = f}) q)}" (is "?L = ?R")
proof -
  {
    fix l
    assume "l ∈ ?L"
    from this[unfolded Lab_lhss_more_def]
    have wf: "funas_term l ⊆ F_all" and q: "map_funs_term UNLAB l ∈ Q" by auto
    from wf have "instance_term l (map_funs_term_wa (λ (f,n). {g. (g,n) ∈ F_all ∧ UNLAB g = f}) (map_funs_term UNLAB l))" 
    proof (induct l)
      case (Var x)
      thus ?case by auto
    next
      case (Fun f ls)
      show ?case
      proof (unfold map_funs_term_wa.simps term.simps instance_term.simps split, intro conjI allI impI, rule, intro conjI)
        fix i
        assume i: "i < length ls"
        hence i': "i < length (map (map_funs_term UNLAB) ls)" by auto
        hence lsi: "ls ! i ∈ set ls" by auto
        from Fun(1)[OF lsi]
        show "instance_term (ls ! i) (map (map_funs_term_wa (λ (f,n). {g. (g,n)  ∈ F_all ∧ UNLAB g = f})) (map (map_funs_term UNLAB) ls) ! i)" unfolding nth_map[OF i'] nth_map[OF i] using Fun(2)[unfolded funas_term.simps set_map set_conv_nth] i
        by force
      qed (insert Fun(2), auto)
    qed
    with q have "l ∈ ?R" by auto
  }
  hence "?L ⊆ ?R" by auto
  moreover
  {
    fix l
    assume "l ∈ ?R"
    then obtain q where q: "q ∈ Q" and inst: "instance_term l (map_funs_term_wa (λ(f,n). {g. (g,n) ∈ F_all ∧ UNLAB g = f}) q)" by auto
    have "l ∈ ?L" unfolding Lab_lhss_more_def
    proof 
      have "funas_term l ⊆ F_all ∧ map_funs_term UNLAB l = q" using inst
      proof (induct l arbitrary: q)
        case (Var x)
        thus ?case by (cases q, auto)
      next
        case (Fun f ss q)
        then obtain g qs where q: "q = Fun g qs" by (cases q, auto)
        note Fun = Fun[unfolded q]
        {
          fix i
          assume i: "i < length ss"
          hence s: "ss ! i ∈ set ss" by auto
          from Fun(2) i
          have inst: "instance_term (ss ! i) (map (map_funs_term_wa (λ(f,n). {g. (g,n) ∈ F_all ∧ UNLAB g = f})) qs ! i)"
            by auto
          from i Fun(2) have i: "i < length qs" by auto
          from Fun(1)[OF s inst[unfolded nth_map[OF i]]]
          have "funas_term (ss ! i) ⊆ F_all ∧ map_funs_term UNLAB (ss ! i) = qs ! i" .
        } note ind = this
        from Fun(2) have len: "length ss = length qs" by auto
        have "map (map_funs_term UNLAB) ss = qs" 
          unfolding map_nth_eq_conv[OF len]
          by (intro allI impI, insert ind len, auto)
        hence "map_funs_term UNLAB (Fun f ss) = q" unfolding q using Fun(2) by auto
        moreover 
        have "funas_term (Fun f ss) ⊆ F_all"
        proof -
          {
            fix s 
            assume "s ∈ set ss"
            from this[unfolded set_conv_nth] ind
            have "funas_term s ⊆ F_all" by force
          }
          with Fun(2) show ?thesis by force
        qed
        ultimately show ?case by simp
      qed
      with q 
      show "funas_term l ⊆ F_all ∧ map_funs_term UNLAB l ∈ Q" by simp
    qed
  }
  ultimately show ?thesis by auto
qed

definition Lab_lhss_more_impl where 
  "Lab_lhss_more_impl LC LS_gen Q ≡ let F_all' = (λ (f,n). map (LC f n) (LS_gen f n)) in concat (map (λ q. flatten_term_enum (map_funs_term_wa F_all' q)) Q)"

definition check_sl_lab_lhss_more :: "('f,'l,'f)lcompose ⇒ 
  ('f ⇒ nat ⇒ 'l list) ⇒ ('f :: show,'v :: show)sl_check1"
  where "check_sl_lab_lhss_more LC LS_gen lQ Q ≡ check_NF_vars_subset (Lab_lhss_more_impl LC LS_gen Q) lQ <+? (λ t. shows_term t +@+ shows '' is missing in labeled Q'')"

locale sl_interpr_root_same_show = sl_interpr_root C c I cge lge L LC LD LS L' LS'
  for  C :: "'c set"
  and  c :: "'c"
  and  I :: "('f :: show,'c)inter"
  and  cge :: "'c ⇒ 'c ⇒ bool"
  and  lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
  and  L :: "('f,'c,'l)label"
  and  LC :: "('f,'l,'f)lcompose"
  and  LD :: "('f,'f,'l)ldecompose"
  and  LS :: "('f,'l)labels" 
  and  L' :: "('f,'c,'l)label"
  and  LS' :: "('f,'l)labels"   
begin

lemma Lab_lhss_more_impl: assumes LS_gen: "⋀ f n. set (LS_gen f n) = Collect (LS f n)"
  shows "set (Lab_lhss_more_impl LC LS_gen Q) = Lab_lhss_more (set Q)"
proof -
  {
    fix f :: 'f and n :: nat
    have "LC f n ` set (LS_gen f n) = {g. (g,n) ∈ F_all ∧ UNLAB g = f}" unfolding LS_gen
      by (auto simp: LD_LC)
  } note id = this
  show ?thesis 
  unfolding Lab_lhss_more_instance_term 
    Lab_lhss_more_impl_def Let_def
  by (auto simp: flatten_term_enum map_funs_term_map_funs_term_wa map_funs_term_wa_compose id)
qed

lemma check_sl_lab_lhss_more: assumes LS_gen: "⋀ f n. set (LS_gen f n) = Collect (LS f n)"
  and check: "isOK(check_sl_lab_lhss_more LC LS_gen lQ Q)"
  shows "NF_terms (Lab_lhss_more (set Q)) ⊇ NF_terms (set lQ)"
proof (rule NF_vars_subset)
  show "NF_vars_subset (Lab_lhss_more (set Q)) (set lQ)"
    using check
    unfolding check_sl_lab_lhss_more_def 
    using Lab_lhss_more_impl[OF LS_gen, of Q] by auto
qed
end



definition check_wf_sym_F_all :: "('f,'l,'lf)lcompose ⇒ ('lf :: show,'f,'l)ldecompose ⇒ ('f,'l)labels ⇒ ('lf × nat) ⇒ shows check"
  where "check_wf_sym_F_all LC LD LS ≡ λ (lf,n). (do {
            let (f,l) = LD lf;
            check (LS f n l ∧ lf = LC f n l) (shows ''labeled symbol '' +@+ shows lf +@+ shows '' not allowed'')
          })"

definition
  check_wf_terms_F_all ::
    "('f, 'l, 'lf) lcompose ⇒ ('lf, 'f, 'l) ldecompose ⇒ ('f, 'l) labels ⇒ ('lf :: show, 'v) term ⇒
      shows check"
where
  "check_wf_terms_F_all LC LD LS lt = do {
    let lfs = funas_term_impl lt;
    check_allm (check_wf_sym_F_all LC LD LS) lfs
  }"
  
lemma (in sl_interpr_root_same_show) check_wf_terms_F_all:
  "isOK (check_wf_terms_F_all LC LD LS lt) ⟷ funas_term lt ⊆ F_all"
proof -
  let ?ft = "funas_term"
  {
    fix lf n
    have "(∃ l f m. (lf,n) = (LC f m l,m) ∧ LS f m l) = isOK(check_wf_sym_F_all LC LD LS (lf,n))" (is "?l = ?r")
    proof -
      obtain f m where LD: "LD lf = (f,m)" by force
      show ?thesis
      proof
        assume ?r
        from this[unfolded check_wf_sym_F_all_def split Let_def LD]
        show ?l by auto
      next
        assume ?l
        then obtain l f where id: "lf = LC f n l" and l: "LS f n l" by auto
        from arg_cong[OF id, of LD, unfolded LD_LC] l id
        show ?r unfolding check_wf_sym_F_all_def by auto
      qed
    qed
  } note main = this
  have "(?ft lt ⊆ F_all) = (∀ lfn ∈ ?ft lt. lfn ∈ F_all)" by auto
  also have "... = isOK(check_wf_terms_F_all LC LD LS lt)"
    unfolding check_wf_terms_F_all_def Let_def using main
    by force
  finally show ?thesis by simp
qed

definition check_Lab_all_trs :: "('f,'l,'f)lcompose ⇒ ('f,'f,'l)ldecompose ⇒ ('f,'l)labels ⇒ ('f :: show,'v :: show)sl_check2"
where "check_Lab_all_trs LC LD LS lR R ≡ do {
  check_allm (λ (l,r). 
    do {
      check_wf_terms_F_all LC LD LS r;
      check (map_funs_rule (λlf. fst (LD lf)) (l,r) ∈ set R)  (shows ''unlabeling of the rule does not yield original rule'')
    } <+? (λs. shows ''problem with labeled rule'' +@+ shows_rule (l,r) +@+ shows_nl +@+ s)
  ) lR
  }"

lemma (in sl_interpr_root_same_show) check_Lab_all_trs: "isOK(check_Lab_all_trs LC LD LS lR R) = (set lR ⊆ Lab_all_trs (set R))"
  unfolding check_Lab_all_trs_def Lab_all_trs_def check_wf_terms_F_all[symmetric] by auto

fun check_sl_decr'_rule :: "('f,'l,'lf)lcompose ⇒ ('lf,'f,'l)ldecompose ⇒ ('f,'l)labels ⇒ 
  ('f ⇒ nat ⇒ 'l ⇒ 'l => bool) ⇒ ('lf,'v)rule ⇒ bool"
  where "check_sl_decr'_rule LC LD LS lge (Fun lf ts, Fun lg us) =
    ( let (f,l1) = LD lf;
          (g,l2) = LD lg;
          n = length ts
        in (f = g ∧ ts = us ∧ lf = LC f n l1 ∧ lg = LC f n l2 ∧ LS f n l1 ∧ LS f n l2 ∧ lge_to_lgr lge LS f n l1 l2))"
  | "check_sl_decr'_rule _ _ _ _ _ = False"

lemma (in sl_interpr) check_sl_decr'_rule: 
  "check_sl_decr'_rule LC LD LS lge lr = (lr ∈ Decr)" 
proof -
  obtain l r where lr: "lr = (l,r)" by force
  show ?thesis
  proof (cases "is_Var l ∨ is_Var r")
    case True
    thus ?thesis
    proof
      assume "is_Var l"
      then obtain x where x: "l = Var x" by auto
      show ?thesis unfolding decr_of_ord_def lr x by auto
    next
      assume "is_Var r"
      then obtain x where x: "r = Var x" by auto
      show ?thesis unfolding decr_of_ord_def lr x by auto
    qed
  next
    case False
    from False obtain lf ts where l: "l = Fun lf ts" by (cases l, auto)
    from False obtain lg us where r: "r = Fun lg us" by (cases r, auto)
    obtain f l1 where lf: "LD lf = (f,l1)" by force    
    obtain g l2 where lg: "LD lg = (g,l2)" by force
    let ?n = "length ts"
    show ?thesis 
      unfolding lr decr_of_ord_def l r
        check_sl_decr'_rule.simps lge_to_lgr_rel_def Let_def lf lg split 
      using lf lg LD_LC by auto
  qed
qed

definition check_sl_decr' :: "('f,'l,'lf)lcompose ⇒ ('lf,'f,'l)ldecompose ⇒ ('f,'l)labels ⇒ 
  ('f ⇒ nat ⇒ 'l ⇒ 'l => bool) ⇒ ('lf :: show,'v :: show)rules ⇒ shows check"
  where "check_sl_decr' LC LD LS lge D ≡ check_allm (λ lr. 
    check (check_sl_decr'_rule LC LD LS lge lr) (shows_rule lr +@+ shows '' is not a decreasing rule'')) D"
  
lemma (in sl_interpr_root_same_show) check_sl_decr': "isOK(check_sl_decr' LC LD LS lge D) = 
   (set D ⊆ Decr)"
  unfolding check_sl_decr'_def using check_sl_decr'_rule by auto

record ('f,'c,'l,'v)sl_ops = 
  sl_L :: "('f,'c,'l)label"
  sl_LS :: "('f,'l)labels" 
  sl_I :: "('f,'c)inter"
  sl_C :: "'c list"
  sl_c :: "'c"
  sl_check_decr :: "('f,'v)rules ⇒ shows check"
  sl_L'' :: "('f,'c,'l)label"
  sl_LS'' :: "('f,'l)labels" 
  sl_lgen :: "'l ⇒ 'l list"
  sl_LS_gen :: "'f ⇒ nat ⇒ 'l list"

(* TODO: think about, whether it is a good idea to add the 
   signature of Q or not (for root-labeling)
   in the following processors
   (since it will produce more rules, it is possible not a good idea)
   (but then default symbol is attached in Q which is also not nice)
*)
definition
  sem_lab_fin_tt ::
    "('f, 'v) splitter ⇒ ('f, 'l, 'f) lcompose ⇒ ('f, 'f, 'l) ldecompose ⇒ 
     ('c ⇒ 'c :: show ⇒ bool) ⇒
     ('tp, 'f :: show, 'v :: show) tp_ops ⇒
     (('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f, 'c, 'l, 'v) sl_ops) ⇒
     ('f, 'v) term list ⇒
     ('f, 'v) rules ⇒ 
     'tp proc"
where
  "sem_lab_fin_tt splitter LC LD cge I gen lQ lAll tp = do {
    ops ← gen (funas_trs_impl (tp_ops.rules I tp)) []; 
    let check_ml = check_sl_model_lab_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_C ops) cge LC;
    let check_d = sl_ops.sl_check_decr ops;
    sem_lab_rel_tt splitter LD I succeed check_d check_ml lQ lAll tp
  }"


definition
  sem_lab_fin_proc ::
    "('f, 'l, 'f) lcompose ⇒ ('f, 'f, 'l) ldecompose ⇒ 
     ('dpp, 'f :: show, 'v :: show) dpp_ops ⇒
     (('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f, 'c :: show, 'l, 'v) sl_ops) ⇒
     ('f, 'v) rules ⇒ 
     ('f, 'v) term list ⇒
     ('f, 'v) rules ⇒ 
     'dpp proc"
where
  "sem_lab_fin_proc LC LD I gen lPAll lQ lRAll dp = do {
    ops ← gen (list_union (funas_trs_impl (dpp_ops.rules I dp)) (funas_args_trs_impl (dpp_ops.pairs I dp))) [];
    let check_q' = check_sl_Q' (sl_ops.sl_I ops) (sl_ops.sl_L ops) LC (sl_ops.sl_C ops);
    let check_ml = check_sl_model_lab_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_C ops) (op =) LC;
    let check_l = check_sl_lab_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_C ops) (op =) LC;
    let check_l' = check_sl_lab' (sl_ops.sl_I ops) (sl_ops.sl_L ops) LC (sl_ops.sl_C ops);
    sem_lab_proc LD I succeed check_q' check_l check_l' check_ml lPAll lQ lRAll dp
  }"

definition
  sem_lab_fin_root_proc ::
    "('f, 'l, 'f) lcompose ⇒ ('f, 'f, 'l) ldecompose ⇒ 
     ('dpp, 'f :: show, 'v :: show) dpp_ops ⇒
     (('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f, 'c :: show, 'l, 'v) sl_ops) ⇒
     ('f, 'v) rules ⇒ 
     ('f, 'v) term list ⇒
     ('f, 'v) rules ⇒ 
     'dpp proc"
where
  "sem_lab_fin_root_proc LC LD I gen lPAll lQ lRAll dp = do {
    let pairs = dpp_ops.pairs I dp;
    ops ← gen (list_union (funas_trs_impl (dpp_ops.rules I dp)) (funas_args_trs_impl pairs)) (roots_trs_impl pairs);
    let check_q' = check_sl_Q' (sl_ops.sl_I ops) (sl_ops.sl_L ops) LC (sl_ops.sl_C ops);
    let check_ml = check_sl_model_lab_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_C ops) (op =) LC;
    let check_l = check_sl_lab_root_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_L'' ops) (sl_ops.sl_C ops) LC;
    let check_l' = check_sl_lab' (sl_ops.sl_I ops) (sl_ops.sl_L ops) LC (sl_ops.sl_C ops);
    sem_lab_root_proc LD I succeed check_q' check_l check_l' check_ml lPAll lQ lRAll dp
  }"

definition
  sem_lab_fin_quasi_root_proc ::
    "('f, 'l, 'f) lcompose ⇒ ('f, 'f, 'l) ldecompose ⇒ 
     ('c ⇒ 'c :: show ⇒ bool) ⇒
     ('f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool) ⇒
     ('dpp, 'f :: show, 'v :: show) dpp_ops ⇒
     (('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f, 'c, 'l, 'v) sl_ops) ⇒
     ('f, 'v) rules ⇒ 
     ('f, 'v) term list ⇒
     ('f, 'v) rules ⇒ 
     'dpp proc"
where
  "sem_lab_fin_quasi_root_proc LC LD cge lge I gen lPAll lQ lRAll dp = do {
    let pairs = dpp_ops.pairs I dp;
    ops ← gen (list_union (funas_trs_impl (dpp_ops.rules I dp)) (funas_args_trs_impl pairs)) (roots_trs_impl pairs);
    let check_d = sl_ops.sl_check_decr ops;
    let check_d' = check_sl_decr' LC LD (sl_ops.sl_LS ops) lge;
    let check_q' = check_sl_lab_lhss_more LC (sl_ops.sl_LS_gen ops);
    let check_ml = check_sl_model_lab_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_C ops) cge LC;
    let check_l = check_sl_lab_all_trs (sl_ops.sl_I ops) (sl_ops.sl_L ops) (sl_ops.sl_L'' ops) (sl_ops.sl_C ops) (sl_ops.sl_lgen ops) LC;
    let check_l' = check_Lab_all_trs LC LD (sl_ops.sl_LS ops);
    sem_lab_quasi_root_proc LD I succeed check_d check_d' check_q' check_l check_l' check_ml lPAll lQ lRAll dp
  }"

locale sl_finite_impl =
 fixes LC :: "('f :: show,'l,'f)lcompose"
   and LD :: "('f,'f,'l)ldecompose"
   and cge :: "'c :: show ⇒ 'c ⇒ bool"
   and lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
   and sl_gen :: "('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f,'c,'l,'v :: show)sl_ops"
 assumes sl_gen_inter: "sl_gen F G = Inr ops ⟹
  sl_interpr_root_same (set (sl_ops.sl_C ops)) (sl_ops.sl_c ops) (sl_ops.sl_I ops) cge lge (sl_ops.sl_L ops) LC LD (sl_ops.sl_LS ops) (sl_ops.sl_L'' ops) (sl_ops.sl_LS'' ops)"
  and sl_gen_decr: "sl_gen F G = Inr ops ⟹
   isOK(sl_ops.sl_check_decr ops D) ⟹ decr_of_ord (lge_to_lgr_rel lge (sl_ops.sl_LS ops)) LC (sl_ops.sl_LS ops) ⊆ (subst.closure (set D) ∩ decr_of_ord (lge_to_lgr_rel lge (sl_ops.sl_LS ops)) LC (sl_ops.sl_LS ops))^+"
  and sl_gen_lgen: "⋀ f n l l'. sl_gen F G = Inr ops ⟹ lge f n l l' ⟹ l' ∈ set (sl_ops.sl_lgen ops l)"
begin

lemma sem_lab_fin_tt: assumes J: "tp_spec J"
  shows "tp_spec.sound_tt_impl J (sem_lab_fin_tt splitter LC LD cge J sl_gen lQ lAll)"
proof -
  interpret tp_spec J by fact
  show ?thesis unfolding sound_tt_impl_def
  proof (clarify)
    fix tp tp'
    assume ok: "sem_lab_fin_tt splitter LC LD cge J sl_gen lQ lAll tp = return tp'"
    and SN: "SN_qrel (tp_ops.qreltrs J tp')"
    note ok = ok[unfolded sem_lab_fin_tt_def]
    let ?F = "funas_trs_impl (tp_ops.rules J tp)"
    from ok obtain ops where gen: "sl_gen ?F [] = Inr ops" 
      by (cases "sl_gen ?F []", auto)
    let ?C = "sl_C ops"
    let ?I = "sl_I ops"
    let ?c = "sl_c ops"
    let ?L = "sl_L ops"
    let ?LS = "sl_LS ops"
    let ?L' = "sl_L'' ops"
    let ?LS' = "sl_LS'' ops"
    let ?cml = "check_sl_model_lab_trs ?I ?L ?C cge LC"
    let ?cd = "sl_check_decr ops"
    from sl_gen_inter[OF gen]
    interpret sl_interpr_root_same "set ?C" ?c ?I cge lge ?L LC LD ?LS ?L' ?LS' .
    interpret sl_interpr_impl "λ _ _. error id" "λ _ _. error id" "λ _ _. error id" "λ _ _.error id" "λ _ _.error id" ?cml "λ _ _. error id" "λ _ _. error id" ?cd "λ _. error id" succeed "set ?C" ?c ?I cge lge ?L ?LS LC LD ?L' ?LS'
      by (unfold_locales, simp, simp, simp, simp, simp, rule
      check_sl_model_lab_trs_sound, insert sl_gen_decr[OF gen], auto)
    from ok[unfolded gen]
    have "sem_lab_rel_tt splitter LD J succeed ?cd
      ?cml lQ lAll tp = Inr tp'" by auto
    with sem_lab_rel_tt[OF J] SN
    show "SN_qrel (tp_ops.qreltrs J tp)"
      unfolding sound_tt_impl_def by blast
  qed
qed

lemma sem_lab_fin_proc: assumes J: "dpp_spec J"
  and cge: "cge = (op =)"
  and lge: "lge = (λ _ _. op =)"
  and inj: "⋀ F G f ops. sl_gen F G = Inr ops ⟹ inj (sl_L ops f)"
  shows "dpp_spec.sound_proc_impl J (sem_lab_fin_proc LC LD J sl_gen lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis unfolding sound_proc_impl_def
  proof (clarify)
    fix dp dp'
    assume ok: "sem_lab_fin_proc LC LD J sl_gen lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    note ok = ok[unfolded sem_lab_fin_proc_def]
    let ?F = "list_union (funas_trs_impl (dpp_ops.rules J dp)) (funas_args_trs_impl (dpp_ops.pairs J dp))"
    let ?G = "[]"
    from ok obtain ops where gen: "sl_gen ?F ?G = Inr ops" 
      by (cases "sl_gen ?F ?G", auto)
    let ?C = "sl_C ops"
    let ?I = "sl_I ops"
    let ?c = "sl_c ops"
    let ?L = "sl_L ops"
    let ?LS = "sl_LS ops"
    let ?L' = "sl_L'' ops"
    let ?LS' = "sl_LS'' ops"
    let ?cml = "check_sl_model_lab_trs ?I ?L ?C (op =) LC"
    let ?cl = "check_sl_lab_trs ?I ?L ?C (op =) LC"
    let ?cl' = "check_sl_lab' ?I ?L LC ?C"
    let ?q' = "check_sl_Q' ?I ?L LC ?C"
    from sl_gen_inter[OF gen, unfolded cge lge]
    interpret sl_interpr_root_same "set ?C" ?c ?I model_cge model_lge ?L LC LD ?LS ?L' ?LS' .
    interpret sl_interpr_impl ?q' ?cl "λ _ _. error id" "λ _ _. error id" ?cl' ?cml "λ _ _. error id" "λ _ _. error id" "λ _. error id" "λ _. error id" succeed "set ?C" ?c ?I model_cge model_lge ?L ?LS LC LD ?L' ?LS'
      by (unfold_locales,  
        rule check_sl_Q', simp,
        rule check_sl_lab_trs_sound, simp,
        simp, simp,
        rule check_sl_lab', simp,
        rule check_sl_model_lab_trs_sound, auto)
    from ok[unfolded gen]
    have "sem_lab_proc LD J succeed
      ?q' ?cl ?cl' ?cml lPAll lQ lRAll dp = Inr dp'" by auto
    with sem_lab_proc[OF J inj[OF gen]] fin
    show "finite_dpp (dpp_ops.dpp J dp)"
      unfolding sound_proc_impl_def by blast
  qed
qed

lemma sem_lab_fin_root_proc: assumes J: "dpp_spec J"
  and cge: "cge = (op =)"
  and lge: "lge = (λ _ _. op =)"
  and inj: "⋀ F G f ops. sl_gen F G = Inr ops ⟹ inj (sl_L ops f)"
  shows "dpp_spec.sound_proc_impl J (sem_lab_fin_root_proc LC LD J sl_gen lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis unfolding sound_proc_impl_def
  proof (clarify)
    fix dp dp'
    assume ok: "sem_lab_fin_root_proc LC LD J sl_gen lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    note ok = ok[unfolded sem_lab_fin_root_proc_def Let_def]
    let ?F = "list_union (funas_trs_impl (dpp_ops.rules J dp)) (funas_args_trs_impl (dpp_ops.pairs J dp))"
    let ?G = "roots_trs_impl (dpp_ops.pairs J dp)"
    from ok obtain ops where gen: "sl_gen ?F ?G = Inr ops" 
      by (cases "sl_gen ?F ?G", auto)
    let ?C = "sl_C ops"
    let ?I = "sl_I ops"
    let ?c = "sl_c ops"
    let ?L = "sl_L ops"
    let ?LS = "sl_LS ops"
    let ?L' = "sl_L'' ops"
    let ?LS' = "sl_LS'' ops"
    let ?cml = "check_sl_model_lab_trs ?I ?L ?C (op =) LC"
    let ?cl = "check_sl_lab_trs ?I ?L ?C (op =) LC"
    let ?clr = "check_sl_lab_root_trs ?I ?L ?L' ?C LC"
    let ?cl' = "check_sl_lab' ?I ?L LC ?C"
    let ?q' = "check_sl_Q' ?I ?L LC ?C"
    from sl_gen_inter[OF gen, unfolded cge lge]
    interpret sl_interpr_root_same "set ?C" ?c ?I model_cge model_lge ?L LC LD ?LS ?L' ?LS' .
    interpret sl_interpr_impl ?q' ?cl ?clr "λ _ _. error id" ?cl' ?cml "λ _ _. error id" "λ _ _. error id" 
      "λ _. error id" "λ _. error id" succeed "set ?C" ?c ?I model_cge model_lge ?L ?LS LC LD ?L' ?LS'
      by (unfold_locales, 
        rule check_sl_Q', simp,
        rule check_sl_lab_trs_sound, simp,
        rule check_sl_lab_root_trs_sound, simp,
        simp,
        rule check_sl_lab', simp,
        rule check_sl_model_lab_trs_sound, auto)
    from ok[unfolded gen]
    have "sem_lab_root_proc LD J succeed
      ?q' ?clr ?cl' ?cml lPAll lQ lRAll dp = Inr dp'" by auto
    with sem_lab_root_proc[OF J inj[OF gen]] fin
    show "finite_dpp (dpp_ops.dpp J dp)"
      unfolding sound_proc_impl_def by blast
  qed
qed
end

locale sl_finite_LS_impl = sl_finite_impl +
 assumes sl_LS_gen: "⋀ f n. sl_gen F G = Inr ops ⟹ set (sl_ops.sl_LS_gen ops f n) = Collect (sl_ops.sl_LS ops f n)"
begin

lemma sem_lab_fin_quasi_root_proc: assumes J: "dpp_spec J"
  shows "dpp_spec.sound_proc_impl J (sem_lab_fin_quasi_root_proc LC LD cge lge J sl_gen lPAll lQ lRAll)"
proof -
  interpret dpp_spec J by fact
  show ?thesis unfolding sound_proc_impl_def
  proof (clarify)
    fix dp dp'
    assume ok: "sem_lab_fin_quasi_root_proc LC LD cge lge J sl_gen lPAll lQ lRAll dp = return dp'"
    and fin: "finite_dpp (dpp_ops.dpp J dp')"
    note ok = ok[unfolded sem_lab_fin_quasi_root_proc_def Let_def]
    let ?F = "list_union (funas_trs_impl (dpp_ops.rules J dp)) (funas_args_trs_impl (dpp_ops.pairs J dp))"
    let ?G = "roots_trs_impl (dpp_ops.pairs J dp)"
    from ok obtain ops where gen: "sl_gen ?F ?G = Inr ops" 
      by (cases "sl_gen ?F ?G", auto)
    let ?C = "sl_C ops"
    let ?I = "sl_I ops"
    let ?c = "sl_c ops"
    let ?L = "sl_L ops"
    let ?LS = "sl_LS ops"
    let ?L' = "sl_L'' ops"
    let ?LS' = "sl_LS'' ops"
    let ?LS_gen = "sl_LS_gen ops"
    let ?lgen = "sl_lgen ops"
    let ?cml = "check_sl_model_lab_trs ?I ?L ?C cge LC"
    let ?cl = "check_sl_lab_trs ?I ?L ?C cge LC"
    let ?cd = "sl_check_decr ops"
    let ?cd' = "check_sl_decr' LC LD ?LS lge"
    let ?clr = "check_sl_lab_all_trs ?I ?L ?L' ?C ?lgen LC"
    let ?cla = "check_Lab_all_trs LC LD ?LS"
    let ?cllm = "check_sl_lab_lhss_more LC ?LS_gen"
    from sl_gen_inter[OF gen]
    interpret sl_interpr_root_same "set ?C" ?c ?I cge lge ?L LC LD ?LS ?L' ?LS' .
    interpret sl_interpr_root_same_show "set ?C" ?c ?I cge lge ?L LC LD ?LS ?L' ?LS' ..
    interpret sl_interpr_impl "λ _ _.error id" ?cl "λ _ _. error id" ?clr "λ _ _. error id" ?cml ?cla ?cllm
      ?cd ?cd' succeed "set ?C" ?c ?I cge lge ?L ?LS LC LD ?L' ?LS'
      by (unfold_locales, 
        simp,
        rule check_sl_lab_trs_sound, simp,
        simp,
        rule check_sl_lab_all_trs_sound[OF _ sl_gen_lgen[OF gen]], simp, simp,
        simp,
        rule check_sl_model_lab_trs_sound, simp,
        unfold check_Lab_all_trs, simp,
        rule check_sl_lab_lhss_more[OF sl_LS_gen[OF gen]], simp,
        rule sl_gen_decr[OF gen], simp,
        unfold check_sl_decr', simp)
    from ok[unfolded gen]
    have "sem_lab_quasi_root_proc LD J succeed ?cd ?cd'
      ?cllm ?clr ?cla ?cml lPAll lQ lRAll dp = Inr dp'" by auto
    with sem_lab_quasi_root_proc[OF J]
    show "finite_dpp (dpp_ops.dpp J dp)"
      using fin
      unfolding sound_proc_impl_def 
      by blast
  qed
qed
end

(* for models, a simplified version can be taken *)
record ('f,'c,'l,'v)slm_ops = 
  slm_L :: "('f,'c,'l)label"
  slm_I :: "('f,'c)inter"
  slm_C :: "'c list"
  slm_c :: "'c"
  slm_L'' :: "('f,'c,'l)label"

definition slm_to_sl :: "('f,'c,'l,'v)slm_ops ⇒ ('f,'c,'l,'v)sl_ops"
  where "slm_to_sl ops ≡ ⦇
    sl_L = slm_ops.slm_L ops,
    sl_LS = λ _ _ _. True,
    sl_I = slm_ops.slm_I ops,
    sl_C = slm_ops.slm_C ops,
    sl_c = slm_ops.slm_c ops,
    sl_check_decr = (λ _.succeed),
    sl_L'' = slm_ops.slm_L'' ops,
    sl_LS'' = λ _ _ _. True,
    sl_lgen = λ l. [l],
    sl_LS_gen = λ _ _. []
  ⦈"

definition slm_gen_to_sl_gen :: "(('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f,'c,'l,'v)slm_ops) ⇒
  ('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f,'c,'l,'v)sl_ops"
where "slm_gen_to_sl_gen gen ≡ λ F G. do { ops ← gen F G; return (slm_to_sl ops)}"


locale sl_finite_model_impl =
 fixes LC :: "('f :: show,'l,'f)lcompose"
   and LD :: "('f,'f,'l)ldecompose"
   and slm_gen :: "('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f,'c :: show,'l,'v :: show)slm_ops"
 assumes LD_LC: "LD (LC f n l) = (f,l)"
  and slm_gen: "slm_gen F G = Inr ops ⟹
  slm_ops.slm_c ops ∈ set (slm_ops.slm_C ops) ∧ wf_inter (slm_ops.slm_I ops) (set (slm_ops.slm_C ops))"
begin

lemma sl_finite_impl: "sl_finite_impl LC LD model_cge model_lge (slm_gen_to_sl_gen slm_gen)"
  unfolding sl_finite_impl_def decr_empty
proof (intro allI impI conjI)
  fix F G ops
  assume ops: "slm_gen_to_sl_gen slm_gen F G = Inr ops"
  then obtain opss where opss: "slm_gen F G = Inr opss"
    unfolding slm_gen_to_sl_gen_def by (cases "slm_gen F G", auto)
  from opss ops have ops: "ops = slm_to_sl opss" 
    unfolding slm_gen_to_sl_gen_def by auto
  show "sl_interpr_root_same (set (sl_C ops)) (sl_c ops) (sl_I ops) model_cge model_lge (sl_L ops) LC LD (sl_LS ops) (sl_L'' ops) (sl_LS'' ops)" unfolding ops slm_to_sl_def sl_ops.simps
    by (unfold_locales, insert slm_gen[OF opss],
      auto simp: wf_label_def cge_wm lge_wm lge_to_lgr_def lge_to_lgr_rel_def LD_LC)
next
  fix F G ops f n and l l' :: 'l
  assume ops: "slm_gen_to_sl_gen slm_gen F G = Inr ops" and id: "l = l'"
  then obtain opss where opss: "slm_gen F G = Inr opss"
    unfolding slm_gen_to_sl_gen_def by (cases "slm_gen F G", auto)
  from opss ops have ops: "ops = slm_to_sl opss" 
    unfolding slm_gen_to_sl_gen_def by auto
  show "l' ∈ set (sl_lgen ops l)" unfolding ops id slm_to_sl_def by auto
qed auto
end

sublocale sl_finite_model_impl ⊆ sl_finite_impl LC LD model_cge model_lge "slm_gen_to_sl_gen slm_gen"
  by (rule sl_finite_impl)

context sl_finite_model_impl
begin
lemma sem_lab_fin_model_proc: assumes J: "dpp_spec J"
  and inj: "⋀ F G ops f. slm_gen F G = Inr ops ⟹ inj (slm_L ops f)"
  shows "dpp_spec.sound_proc_impl J (sem_lab_fin_proc LC LD J (slm_gen_to_sl_gen slm_gen) lPAll lQ lRAll)"
proof (rule sem_lab_fin_proc[OF J refl refl])
  fix F G f ops
  assume "slm_gen_to_sl_gen slm_gen F G = Inr ops"
  thus "inj (sl_L ops f)"
    unfolding slm_gen_to_sl_gen_def inj_on_def
    by (cases "slm_gen F G", insert inj[unfolded inj_on_def], auto simp: slm_to_sl_def)
qed

lemma sem_lab_fin_model_root_proc: assumes J: "dpp_spec J"
  and inj: "⋀ F G ops f. slm_gen F G = Inr ops ⟹ inj (slm_L ops f)"
  shows "dpp_spec.sound_proc_impl J (sem_lab_fin_root_proc LC LD J (slm_gen_to_sl_gen slm_gen) lPAll lQ lRAll)"
proof (rule sem_lab_fin_root_proc[OF J refl refl])
  fix F G f ops
  assume "slm_gen_to_sl_gen slm_gen F G = Inr ops"
  thus "inj (sl_L ops f)"
    unfolding slm_gen_to_sl_gen_def inj_on_def
    by (cases "slm_gen F G", insert inj[unfolded inj_on_def], auto simp: slm_to_sl_def)
qed
end

end