Theory ORD_RES_2

theory ORD_RES_2
  imports
    ORD_RES
    Exhaustive_Factorization
begin

section ‹ORD-RES-2 (full factorization)›

context simulation_SCLFOL_ground_ordered_resolution begin

inductive ord_res_2 where
  factoring: "
    is_least_false_clause (N |∪| U⇩r |∪| U⇩e⇩f) C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_pos L ⟹
    U⇩e⇩f' = finsert (efac C) U⇩e⇩f ⟹
    ord_res_2 N (U⇩r, U⇩e⇩f) (U⇩r, U⇩e⇩f')" |

  resolution: "
    is_least_false_clause (N |∪| U⇩r |∪| U⇩e⇩f) C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    D |∈| N |∪| U⇩r |∪| U⇩e⇩f ⟹
    D ≺⇩c C ⟹
    ord_res.production (fset (N |∪| U⇩r |∪| U⇩e⇩f)) D = {atm_of L} ⟹
    ord_res.ground_resolution C D CD ⟹
    U⇩r' = finsert CD U⇩r ⟹
    ord_res_2 N (U⇩r, U⇩e⇩f) (U⇩r', U⇩e⇩f)"

inductive ord_res_2_step where
  "ord_res_2 N S S' ⟹ ord_res_2_step (N, S) (N, S')"

inductive ord_res_2_final where
  "ord_res_final (N |∪| U⇩r |∪| U⇩e⇩f) ⟹ ord_res_2_final (N, (U⇩r, U⇩e⇩f))"

inductive ord_res_2_load where
  "N ≠ {||} ⟹ ord_res_2_load N (N, ({||}, {||}))"

sublocale ord_res_2_semantics: semantics where
  step = ord_res_2_step and
  final = ord_res_2_final
proof unfold_locales
  fix S :: "'f gterm clause fset × 'f gterm clause fset × 'f gterm clause fset"

  obtain N U⇩r U⇩e⇩f :: "'f gterm clause fset" where
    S_def: "S = (N, (U⇩r, U⇩e⇩f))"
    by (metis prod.exhaust)

  assume "ord_res_2_final S"
  hence "{#} |∈| N |∪| U⇩r |∪| U⇩e⇩f ∨ ¬ ex_false_clause (fset (N |∪| U⇩r |∪| U⇩e⇩f))"
    by (simp add: S_def ord_res_2_final.simps ord_res_final_def)
  thus "finished ord_res_2_step S"
  proof (elim disjE)
    assume "{#} |∈| N |∪| U⇩r |∪| U⇩e⇩f"
    have False if "ord_res_2 N (U⇩r, U⇩e⇩f) x" for x
      using that[unfolded S_def]
    proof (cases N "(U⇩r, U⇩e⇩f)" x rule: ord_res_2.cases)
      case hyps: (factoring C L U⇩e⇩f')
      from hyps have "C = {#}"
        using is_least_false_clause_mempty[OF ‹{#} |∈| N |∪| U⇩r |∪| U⇩e⇩f›]
        by (metis Uniq_D Uniq_is_least_false_clause)
      moreover from hyps have "L ∈# C"
        using linorder_lit.is_maximal_in_mset_iff by blast
      ultimately show False
        by simp
    next
      case hyps: (resolution C L D CD U⇩e⇩f')
      from hyps ‹{#} |∈| N |∪| U⇩r |∪| U⇩e⇩f› have "C = {#}"
        using is_least_false_clause_mempty[OF ‹{#} |∈| N |∪| U⇩r |∪| U⇩e⇩f›]
        by (metis Uniq_D Uniq_is_least_false_clause)
      moreover from hyps have "L ∈# C"
        using linorder_lit.is_maximal_in_mset_iff by blast
      ultimately show False
        by simp
    qed
    thus "finished ord_res_2_step S"
      unfolding finished_def ord_res_2_step.simps S_def
      by (metis prod.inject)
  next
    assume no_false_cls: "¬ ex_false_clause (fset (N |∪| U⇩r |∪| U⇩e⇩f))"
    have False if "ord_res_2 N (U⇩r, U⇩e⇩f) x" for x
      using that[unfolded S_def]
    proof (cases N "(U⇩r, U⇩e⇩f)" x rule: ord_res_2.cases)
      case hyps: (factoring C L U⇩e⇩f')
      thus False
        using no_false_cls[unfolded ex_false_clause_def]
        using is_least_false_clause_def linorder_cls.is_least_in_fset_iff by auto
    next
      case hyps: (resolution C L D CD U⇩e⇩f')
      thus False
        using no_false_cls[unfolded ex_false_clause_def]
        using is_least_false_clause_def linorder_cls.is_least_in_fset_iff by auto
    qed
    thus "finished ord_res_2_step S"
      unfolding finished_def ord_res_2_step.simps S_def
      by (metis prod.inject)
  qed
qed

sublocale ord_res_2_language: language where
  step = ord_res_2_step and
  final = ord_res_2_final and
  load = ord_res_2_load
  by unfold_locales

lemma is_least_in_fset_with_irrelevant_clauses_if_is_least_in_fset:
  assumes
    irrelevant: "∀D |∈| N'. ∃E |∈| N. E ⊂# D ∧ set_mset D = set_mset E" and
    C_least: "linorder_cls.is_least_in_fset {|C |∈| N. ¬ ord_res_Interp (fset N) C ⊫ C|} C"
  shows "linorder_cls.is_least_in_fset {|C |∈| N |∪| N'. ¬ ord_res_Interp (fset (N |∪| N')) C ⊫ C|} C"
proof -
  have
    C_in: "C |∈| N" and
    C_not_entailed: "¬ ord_res_Interp (fset N) C ⊫ C" and
    C_lt: "∀x |∈| N. x ≠ C ⟶ ¬ ord_res_Interp (fset N) x ⊫ x ⟶ C ≺⇩c x"
    using C_least linorder_cls.is_least_in_ffilter_iff by simp_all

  have "C |∈| N |∪| N'"
    using C_in by simp

  moreover have "¬ ord_res_Interp (fset (N |∪| N')) C ⊫ C"
    using extended_partial_model_entails_iff_partial_model_entails[
        of "fset N" "fset N'", OF finite_fset finite_fset irrelevant]
    using C_in C_not_entailed
    by simp

  moreover have "C ≺⇩c x"
    if
      x_in: "x |∈| N |∪| N'" and
      x_neq: "x ≠ C" and
      x_not_entailed: "¬ ord_res_Interp (fset (N |∪| N')) x ⊫ x"
    for x
  proof -

    from x_in have "x |∈| N ∨ x |∈| N'"
      by simp
    thus "C ≺⇩c x"
    proof (elim disjE)
      assume x_in: "x |∈| N"

      moreover have "¬ ord_res_Interp (fset N) x ⊫ x"
        using extended_partial_model_entails_iff_partial_model_entails[
            of "fset N" "fset N'", OF finite_fset finite_fset irrelevant x_in]
        using x_not_entailed by simp

      ultimately show "C ≺⇩c x"
        using C_lt[rule_format, of x] x_neq by argo
    next
      assume "x |∈| N'"
      then obtain x' where "x' |∈| N" and "x' ⊂# x" "set_mset x' = set_mset x"
        using irrelevant by metis

      have "x' ≺⇩c x"
        using ‹x' ⊂# x› by (metis strict_subset_implies_multp)

      moreover have "C ≼⇩c x'"
      proof (cases "x' = C")
        case True
        thus ?thesis
          by order
      next
        case False

        have "C ≺⇩c x'"
        proof (rule C_lt[rule_format])
          show "x' |∈| N"
            using ‹x' |∈| N› .
        next
          show "x' ≠ C"
            using False .
        next
          have "¬ ord_res_Interp (fset (N |∪| N')) x ⊫ x'"
            using x_not_entailed ‹set_mset x' = set_mset x›
            by (metis true_cls_def)
          hence "¬ ord_res_Interp (fset (N |∪| N')) x' ⊫ x'"
            by (metis ‹x' ≺⇩c x› ord_res.entailed_clause_stays_entailed)
          thus "¬ ord_res_Interp (fset N) x' ⊫ x'"
            using extended_partial_model_entails_iff_partial_model_entails[
                of "fset N" "fset N'" x', OF finite_fset finite_fset irrelevant]
            using ‹x' |∈| N› by simp
        qed
        thus ?thesis
          by order
      qed

      ultimately show "C ≺⇩c x"
        by order
    qed
  qed

  ultimately show "linorder_cls.is_least_in_fset {|C |∈| N |∪| N'.
    ¬ ord_res_Interp (fset (N |∪| N')) C ⊫ C|} C"
    using C_in C_not_entailed
    unfolding linorder_cls.is_least_in_ffilter_iff by metis
qed

primrec fset_upto :: "nat ⇒ nat ⇒ nat fset" where
  "fset_upto i 0 = (if i = 0 then {|0|} else {||})" |
  "fset_upto i (Suc n) = (if i ≤ Suc n then finsert (Suc n) (fset_upto i n) else {||})"

lemma
  "fset_upto 0 0 = {|0|}"
  "fset_upto 0 1 = {|0, 1|}"
  "fset_upto 0 2 = {|0, 1, 2|}"
  "fset_upto 0 3 = {|0, 1, 2, 3|}"
  "fset_upto 1 3 = {|1, 2, 3|}"
  "fset_upto 2 3 = {|2, 3|}"
  "fset_upto 3 3 = {|3|}"
  "fset_upto 4 3 = {||}"
  unfolding numeral_2_eq_2 numeral_3_eq_3
  by auto

lemma "i ≤ 1 + j ⟹ List.upto i (1 + j) = List.upto i j @ [1 + j]"
  using upto_rec2 by simp

lemma fset_of_append_singleton: "fset_of_list (xs @ [x]) = finsert x (fset_of_list xs)"
  by simp

lemma "fset_of_list (List.upto (int i) (int j)) = int |`| fset_upto i j"
proof (induction j)
  case 0
  show ?case
    by simp
next
  case (Suc j)
  show ?case
  proof (cases "i ≤ Suc j")
    case True
    hence AAA: "int i ≤ 1 + int j"
      by presburger

    from True show ?thesis
      apply simp
      unfolding Suc.IH[symmetric]
      unfolding upto_rec2[OF AAA] fset_of_append_singleton
      by simp
  next
    case False
    thus ?thesis
      by simp
  qed
qed

lemma fset_fset_upto[simp]: "fset (fset_upto m n) = {m..n}"
  apply (induction n)
  apply simp
  apply simp
  using atLeastAtMostSuc_conv by presburger

lemma minus_mset_replicate_strict_subset_minus_msetI:
  assumes "m < n" and "n < count C L"
  shows "C - replicate_mset n L ⊂# C - replicate_mset m L"
proof -
  from ‹m < n› obtain k1 where n_def: "n = m + Suc k1"
    using less_natE by auto

  with ‹n < count C L› obtain k2 where
    count_eq: "count C L = m + Suc k1 + Suc k2"
    by (metis add.commute add_Suc group_cancel.add1 less_natE)

  define C⇩0 where
    "C⇩0 = {#K ∈# C. K ≠ L#}"

  have C_eq: "C = C⇩0 + replicate_mset m L + replicate_mset (Suc k1) L + replicate_mset (Suc k2) L"
    using C⇩0_def count_eq
    by (metis (mono_tags, lifting) filter_mset_eq group_cancel.add1 replicate_mset_plus
        union_filter_mset_complement)

  have "C - replicate_mset n L = C⇩0 + replicate_mset (Suc k2) L"
    unfolding C_eq n_def
    by (simp add: replicate_mset_plus)
  also have "… ⊂# C⇩0 + replicate_mset (Suc k1) L + replicate_mset (Suc k2) L"
    by simp
  also have "… = C - replicate_mset m L"
    unfolding C_eq
    by (simp add: replicate_mset_plus)
  finally show ?thesis .
qed

lemma factoring_all_is_between_efac_and_original_clause:
  fixes z
  assumes
    "is_pos L" and "ord_res.is_maximal_lit L C" and "count C L = Suc (Suc n)"
    "m' ≤ n" and
    z_in: "z |∈| (λi. C - replicate_mset i L) |`| fset_upto 0 m'"
  shows "efac C ⊂# z" and "z ⊆# C"
proof -
  from z_in obtain i where
    "i ≤ m'" and
    z_def: "z = C - replicate_mset i L"
    by auto

  have "i ≤ n"
    using ‹i ≤ m'› ‹m' ≤ n› by presburger
  hence "i < count C L"
    using ‹count C L = Suc (Suc n)› by presburger
  thus "z ⊆# C"
    unfolding z_def by simp

  show "efac C ⊂# z"
  proof -
    have "efac C = add_mset L {#K ∈# C. K ≠ L#}"
      using efac_spec_if_pos_lit_is_maximal[OF ‹is_pos L› ‹ord_res.is_maximal_lit L C›] .
    also have "… ⊂# add_mset L (add_mset L {#K ∈# C. K ≠ L#})"
      by simp
    also have "… = C - replicate_mset n L"
      using minus_mset_replicate_mset_eq_add_mset_add_mset_filter_mset[
          OF ‹count C L = Suc (Suc n)›] ..
    also have "… ⊆# C - replicate_mset i L"
      using ‹i ≤ n› by (simp add: subseteq_mset_def)
    also have "… = z"
      using z_def ..
    finally show ?thesis .
  qed
qed

lemma
  assumes
    "linorder_cls.is_least_in_fset {|x |∈| N1. P N1 x|} x" and
    "linorder_cls.is_least_in_fset N2 y" and
    "∀z |∈| N2. z ≼⇩c x" and
    "P (N1 |∪| N2) y" and
    "∀z |∈| N1. z ≺⇩c x ⟶ ¬ P (N1 |∪| N2) z"
  shows "linorder_cls.is_least_in_fset {|x |∈| N1 |∪| N2. P (N1 |∪| N2) x|} y"
proof -
  show ?thesis
    unfolding linorder_cls.is_least_in_ffilter_iff
  proof (intro conjI ballI impI)
    from assms(2) show "y |∈| N1 |∪| N2"
      unfolding linorder_cls.is_least_in_fset_iff by simp
  next
    from assms(4) show "P (N1 |∪| N2) y"
      by argo
  next
    fix z
    assume z_in: "z |∈| N1 |∪| N2" and "z ≠ y" and "P (N1 |∪| N2) z"
    show "y ≺⇩c z"
      using z_in[unfolded funion_iff]
    proof (elim disjE)
      from assms(2,3,5) show "z |∈| N1 ⟹ y ≺⇩c z"
        by (metis ‹P (N1 |∪| N2) z› ‹z ≠ y› linorder_cls.dual_order.not_eq_order_implies_strict
            linorder_cls.is_least_in_fset_iff linorder_cls.less_linear
            linorder_cls.order.strict_trans)
    next
      from assms(2) show "z |∈| N2 ⟹ y ≺⇩c z"
        using ‹z ≠ y› linorder_cls.is_least_in_fset_iff by blast
    qed
  qed
qed

lemma ground_factoring_preserves_efac:
  assumes "ord_res.ground_factoring P C"
  shows "efac P = efac C"
  using assms
  by (smt (verit, ccfv_threshold) filter_mset_add_mset is_pos_def ord_res.ground_factoring.cases
      ord_res.ground_factoring_preserves_maximal_literal efac_spec_if_pos_lit_is_maximal)

lemma ground_factorings_preserves_efac:
  assumes "ord_res.ground_factoring⇧*⇧* P C"
  shows "efac P = efac C"
  using assms
  by (induction P rule: converse_rtranclp_induct)
    (simp_all add: ground_factoring_preserves_efac)


lemma ex_ord_res_2_if_not_final:
  assumes "¬ ord_res_2_final S"
  shows "∃S'. ord_res_2_step S S'"
proof -
  from assms obtain N U⇩r U⇩e⇩f where
    S_def: "S = (N, (U⇩r, U⇩e⇩f))" and
    "{#} |∉| N |∪| U⇩r |∪| U⇩e⇩f" and
    "ex_false_clause (fset (N |∪| U⇩r |∪| U⇩e⇩f))"
    by (metis ord_res_2_final.intros ord_res_final_def surj_pair)

  obtain C where C_least_false: "is_least_false_clause (N |∪| U⇩r |∪| U⇩e⇩f) C"
    using ‹ex_false_clause (fset (N |∪| U⇩r |∪| U⇩e⇩f))› obtains_least_false_clause_if_ex_false_clause
    by metis

  hence "C ≠ {#}"
    using ‹{#} |∉| N |∪| U⇩r |∪| U⇩e⇩f›
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    by metis

  then obtain L where C_max: "linorder_lit.is_maximal_in_mset C L"
    using linorder_lit.ex_maximal_in_mset by metis

  show ?thesis
  proof (cases L)
    case (Pos A)
    thus ?thesis
      using ord_res_2.factoring[OF C_least_false C_max] S_def is_pos_def
      by (metis ord_res_2_step.intros)
  next
    case (Neg A)
    then obtain D where
      "D |∈| N |∪| U⇩r |∪| U⇩e⇩f" and
      "D ≺⇩c C" and
      "ord_res.is_strictly_maximal_lit (Pos A) D" and
      "ord_res.production (fset (N |∪| U⇩r |∪| U⇩e⇩f)) D = {A}"
      using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
      using C_least_false C_max by metis

    moreover then obtain CD where
      "ord_res.ground_resolution C D CD"
      using ex_ground_resolutionI C_max Neg by metis

    ultimately show ?thesis
      using ord_res_2.resolution[OF C_least_false C_max]
      by (metis Neg S_def literal.disc(2) literal.sel(2) ord_res_2_step.intros)
  qed
qed

corollary ord_res_2_step_safe: "ord_res_2_final S ∨ (∃S'. ord_res_2_step S S')"
  using ex_ord_res_2_if_not_final by metis

lemma is_least_false_clause_if_is_least_false_clause_in_union_unproductive:
  assumes
    N2_unproductive: "∀C |∈| N2. ord_res.production (fset (N1 |∪| N2)) C = {}" and
    C_in: "C |∈| N1" and
    C_least_false: "is_least_false_clause (N1 |∪| N2) C"
  shows "is_least_false_clause N1 C"
  unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
proof (intro conjI ballI impI)
  show "C |∈| N1"
    using C_in .
next
  have "¬ ord_res_Interp (fset (N1 |∪| N2)) C ⊫ C"
    using C_least_false[unfolded is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff]
    by argo
  thus "¬ ord_res.interp (fset N1) C ∪ ord_res.production (fset N1) C ⊫ C"
    unfolding Interp_union_unproductive[of "fset N1" "fset N2", folded union_fset,
        OF finite_fset finite_fset N2_unproductive] .
next
  fix D
  have "∀D |∈| N1 |∪| N2. D ≠ C ⟶ ¬ ord_res_Interp (fset (N1 |∪| N2)) D ⊫ D ⟶ C ≺⇩c D"
    using C_least_false[unfolded is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff]
    by argo

  moreover assume "D |∈| N1" and "D ≠ C" and "¬ ord_res_Interp (fset N1) D ⊫ D"

  ultimately show "C ≺⇩c D"
    using Interp_union_unproductive[of "fset N1" "fset N2", folded union_fset,
        OF finite_fset finite_fset N2_unproductive]
    by simp
qed

lemma ground_factoring_replicate_max_pos_lit:
  "ord_res.ground_factoring
    (C⇩0 + replicate_mset (Suc (Suc n)) (Pos A))
    (C⇩0 + replicate_mset (Suc n) (Pos A))"
  if "ord_res.is_maximal_lit (Pos A) (C⇩0 + replicate_mset (Suc (Suc n)) (Pos A))"
  for A C⇩0 n
proof (rule ord_res.ground_factoringI)
  show "C⇩0 + replicate_mset (Suc (Suc n)) (Pos A) =
            add_mset (Pos A) (add_mset (Pos A) (C⇩0 + replicate_mset n (Pos A)))"
    by simp
next
  show "ord_res.is_maximal_lit (Pos A) (C⇩0 + replicate_mset (Suc (Suc n)) (Pos A))"
    using that .
next
  show "C⇩0 + replicate_mset (Suc n) (Pos A) =
            add_mset (Pos A) (C⇩0 + replicate_mset n (Pos A))"
    by simp
qed simp

lemma ground_factorings_replicate_max_pos_lit:
  assumes
    "ord_res.is_maximal_lit (Pos A) (C⇩0 + replicate_mset (Suc (Suc n)) (Pos A))"
  shows "m ≤ Suc n ⟹ (ord_res.ground_factoring ^^ m)
    (C⇩0 + replicate_mset (Suc (Suc n)) (Pos A))
    (C⇩0 + replicate_mset (Suc (Suc n - m)) (Pos A))"
proof (induction m)
  case 0
  show ?case
    by simp
next
  case (Suc m')
  then show ?case
    apply (cases m')
    using assms ground_factoring_replicate_max_pos_lit apply auto[1]
    by (metis (no_types, lifting) Suc_diff_le Suc_leD assms diff_Suc_Suc
        ground_factoring_replicate_max_pos_lit ord_res.ground_factorings_preserves_maximal_literal
        relpowp_Suc_I relpowp_imp_rtranclp)
qed

lemma ord_res_Interp_entails_if_greatest_lit_is_pos:
  assumes C_in: "C ∈ N" and L_greatest: "linorder_lit.is_greatest_in_mset C L" and L_pos: "is_pos L"
  shows "ord_res_Interp N C ⊫ C"
proof (cases "ord_res.interp N C ⊫ C")
  case True
  hence "ord_res.production N C = {}"
    by (simp add: ord_res.production_unfold)
  with True show ?thesis
    by simp
next
  case False

  from L_pos obtain A where L_def: "L = Pos A"
    by (cases L) simp_all

  from L_greatest obtain C' where C_def: "C = add_mset L C'"
    unfolding linorder_lit.is_greatest_in_mset_iff
    by (metis insert_DiffM)

  with C_in L_greatest have "A ∈ ord_res.production N C"
    unfolding L_def ord_res.production_unfold
    using False
    by (simp add: linorder_lit.is_greatest_in_mset_iff multi_member_split)
  thus ?thesis
    by (simp add: true_cls_def C_def L_def)
qed

lemma right_unique_ord_res_2: "right_unique (ord_res_2 N)"
proof (rule right_uniqueI)
  fix s s' s'' :: "'f gterm clause fset × 'f gterm clause fset"
  assume step1: "ord_res_2 N s s'" and step2: "ord_res_2 N s s''"
  show "s' = s''"
    using step1
  proof (cases N s s' rule: ord_res_2.cases)
    case hyps1: (factoring U⇩r1 U⇩e⇩f1 C1 L1 U⇩e⇩f'1)
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_2.cases)
      case (factoring U⇩r2 U⇩e⇩f2 C2 L2 U⇩e⇩f'2)
      with hyps1 show ?thesis
        by (metis Uniq_D Uniq_is_least_false_clause prod.inject)
    next
      case (resolution U⇩r U⇩e⇩f C L D CD U⇩r')
      with hyps1 have False
        by (metis Pair_inject Uniq_is_least_false_clause linorder_lit.Uniq_is_maximal_in_mset
            the1_equality')
      thus ?thesis ..
    qed
  next
    case hyps1: (resolution U⇩r1 U⇩e⇩f1 C1 L1 D1 CD1 U⇩r'1)
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_2.cases)
      case (factoring U⇩r2 U⇩e⇩f2 C2 L2 U⇩e⇩f'2)
      with hyps1 have False
        by (metis Pair_inject Uniq_is_least_false_clause linorder_lit.Uniq_is_maximal_in_mset
            the1_equality')
      thus ?thesis ..
    next
      case (resolution U⇩r U⇩e⇩f C L D CD U⇩r')
      with hyps1 show ?thesis
        by (metis (mono_tags, lifting) Uniq_is_least_false_clause
            linorder_lit.Uniq_is_maximal_in_mset ord_res.Uniq_production_eq_singleton
            ord_res.unique_ground_resolution prod.inject the1_equality')
    qed
  qed
qed

lemma right_unique_ord_res_2_step: "right_unique ord_res_2_step"
proof (rule right_uniqueI)
  fix x y z
  show "ord_res_2_step x y ⟹ ord_res_2_step x z ⟹ y = z"
    apply (cases x; cases y; cases z)
    apply (simp add: ord_res_2_step.simps)
    using right_unique_ord_res_2[THEN right_uniqueD]
    by blast
qed

end

end