section ‹Reflection of confluence by currying›
theory LS_Currying2
imports LS_Currying
begin
context pp_cr
begin
lemma missing_persists_Cu [simp]:
assumes "is_Fun l"
shows "missing_args (mctxt_of_term ((Cu l) ⋅ σ)) n = missing_args (mctxt_of_term (l ⋅ σ)) n"
using assms
proof (induction l arbitrary: n)
case (Fun f ts)
{ fix x
assume asm: "x ∈ set ts"
have "missing_args (mctxt_of_term (x ⋅ σ)) n' =
missing_args (mctxt_of_term ((Cu x) ⋅ σ)) n'" for n'
using Fun(1)[OF asm, of n'] by (cases x) simp+
} note inner = this
thus ?case
proof (cases "f = Ap")
case isAp: True
thus ?thesis using inner isAp by simp
next
case notAp: False
hence "Suc (arity f) - length (map mctxt_of_term ts) - n =
missing_args (mctxt_of_term (Cu (Fun f ts) ⋅ σ)) n"
using inner
proof (induction "length ts" arbitrary: n ts)
case (Suc n')
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have "Suc (arity f) - Suc (length (map mctxt_of_term ts')) - n =
missing_args (mctxt_of_term (Cu (Fun f ts') ⋅ σ)) (Suc n)"
using Suc(1)[OF _ Suc(3), of ts' "Suc n"] Suc(2,4)
unfolding ts_def by simp
then show ?case using Suc(2-) unfolding ts_def by simp
qed simp
thus ?thesis using notAp by force
qed
qed simp
lemma check_persists_Cu [simp]:
assumes "is_Fun l"
shows "check_first_non_Ap n ((Cu l) ⋅ σ) = check_first_non_Ap n (l ⋅ σ)"
using missing_args_unfold missing_persists_Cu[OF assms] by metis
lemma ℱ_in_𝔏⇩1:
assumes "funas_term t ⊆ ℱ⇩U - { (Ap, 2) }"
shows "𝔏⇩1 (mctxt_of_term t)"
using assms
proof (induction t)
case (Fun f ts)
moreover have "x ∈ set ts ⟶ 𝔏⇩1 (mctxt_of_term x)" for x using Fun by auto
ultimately show ?case using Fun(2) 𝔏⇩1.simps[of "MFun f (map mctxt_of_term ts)"] by simp
qed auto
lemma Cu_ℱ_𝔏⇩1:
assumes "funas_term t ⊆ ℱ⇩U - { (Ap, 2) }"
shows "𝔏⇩1 (mctxt_of_term (Cu t))"
proof -
have "𝔏⇩1 (mctxt_of_term t)" using ℱ_in_𝔏⇩1[OF assms] .
thus ?thesis using assms
proof (induction t)
case (Fun f ts) thus ?case
proof (induction "length ts" arbitrary: ts)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have arity_f: "length ts ≤ arity f"
using Suc(5) unfolding ℱ⇩U_def arity_def by fastforce
have "f ≠ Ap" using Suc(5) fresh unfolding ℱ⇩U_def by fastforce
have f_ts': "(f, length ts') ∈ ℱ⇩U - {(Ap, 2)}"
using ℱ⇩U_def ℱ_def Suc(5) fresh unfolding ts_def by force
have "x ∈ set ts ⟶ 𝔏⇩1 (mctxt_of_term x)" for x
using Suc(4) 𝔏_def in_set_idx sub_layers by fastforce
hence "x ∈ set ts' ⟶ 𝔏⇩1 (mctxt_of_term x)" for x unfolding ts_def by simp
hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Fun f ts'))"
using Suc(4) f_ts' unfolding ts_def mctxt_of_term.simps by fastforce
have funas: "funas_term (Fun f ts') ⊆ ℱ⇩U - {(Ap, 2)}"
using Suc(5) ‹f ≠ Ap› unfolding ts_def ℱ⇩U_def by auto
have arg1: "𝔏⇩1 (mctxt_of_term (Cu (Fun f ts')))"
using Suc(1)[OF _ _ in_𝔏⇩1 funas] Suc(2,3) unfolding ts_def by force
have "check_first_non_Ap 1 (Fun f ts')"
using arity_f ‹f ≠ Ap› unfolding ts_def by simp
hence "check_first_non_Ap 1 (Cu (Fun f ts'))"
using check_persists_Cu[of "Fun f ts'" 1 Var] by simp
moreover have arg2: "𝔏⇩1 (mctxt_of_term (Cu a))"
using Suc(3)[of a] Suc(5) ℱ_in_𝔏⇩1[of a] unfolding ts_def by auto
ultimately show ?case using ‹f ≠ Ap› arg1
unfolding ts_def missing_args_unfold[symmetric] by auto
qed simp
qed simp
qed
lemma Cu⇩R_NF_𝒰_ℛ_step:
assumes "(Cu s, Cu t) ∈ rstep (Cu⇩R ℛ)" "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
shows "(s, t) ∈ rstep ℛ"
proof -
obtain C l r σ where s_def: "Cu s = C⟨l ⋅ σ⟩" and t_def: "Cu t = C⟨r ⋅ σ⟩" and
in_Cu⇩R: "(l, r) ∈ Cu⇩R ℛ"
using assms(1) by fast
then obtain l' r' where l_def: "l = Cu l'" and r_def: "r = Cu r'" and in_ℛ: "(l', r') ∈ ℛ"
using Cu⇩R_def by auto
obtain f ts' where l'_def: "l' = Fun f ts'" using in_ℛ wfR unfolding wf_trs_def
by fastforce
hence "f ≠ Ap" "arity f = length ts'" using in_ℛ sigR fresh
unfolding arity_def funas_trs_def funas_rule_def by fastforce+
moreover obtain ts where lσ_def: "l' ⋅ σ = Fun f ts" "length ts = length ts'"
using l'_def by auto
ultimately have "¬ check_first_non_Ap 1 (l' ⋅ σ)" by auto
hence check_lσ: "¬ check_first_non_Ap 1 (l ⋅ σ)"
using check_persists_Cu[of l' 1 σ] unfolding l_def by fastforce
have Cu_s_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Cu s))"
using Cu_ℱ_𝔏⇩1[of s] assms(2) fresh unfolding ℱ_def ℱ⇩U_def by auto
{ fix C' f' ss2
assume "C = C' ∘⇩c More f' [] □ ss2"
hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Fun f' ([] @ l ⋅ σ # ss2)))"
using Cu_s_𝔏⇩1 subm_at_layers[of "mctxt_of_term (Cu s)" "hole_pos C'"] unfolding s_def 𝔏_def
by simp (metis hole_pos_poss list.simps(9) mctxt_of_term.simps(2)
subm_at.simps(1) subm_at_mctxt_of_term subt_at_hole_pos)
have "f' ≠ Ap" using 𝔏⇩1.cases[OF in_𝔏⇩1] check_lσ fresh
unfolding missing_args_unfold[symmetric] ℱ⇩U_def by simp ((cases "f' = Ap"), fastforce)
}
hence no_Ap_above: "∀C' f ss2. C = C' ∘⇩c More f [] □ ss2 ⟶ f ≠ Ap"
by blast
obtain D where "NF_𝒰 (Cu s) = D⟨NF_𝒰 (l ⋅ σ)⟩ ∧ NF_𝒰 (Cu t) = D⟨NF_𝒰 (r ⋅ σ)⟩"
using NF_𝒰_persists[OF no_Ap_above]
unfolding s_def t_def by blast
moreover have "funas_term l' ⊆ ℱ" "funas_term r' ⊆ ℱ" using in_ℛ sigR ℱ_def
unfolding funas_trs_def funas_rule_def by fastforce+
ultimately have s_def: "s = D⟨l' ⋅ (NF_𝒰 ∘ σ)⟩" and NF_𝒰_t_def: "t = D⟨r' ⋅ (NF_𝒰 ∘ σ)⟩"
using NF_𝒰_Cu_subst[of _ σ] NF_𝒰_Cu assms(2,3) unfolding l_def r_def by auto
moreover have "(s, t) ∈ rstep ℛ" unfolding s_def NF_𝒰_t_def using in_ℛ by blast
ultimately show ?thesis by blast
qed
inductive is_Cu' :: "('f, 'v) term ⇒ nat ⇒ bool" where
var [intro]: "is_Cu' (Var x) 0"
| funs [intro]: "sigF f = Some n ⟹ is_Cu' (Fun f []) n"
| ap [intro]: "is_Cu' t⇩1 (Suc n) ⟹ is_Cu' t⇩2 0 ⟹ is_Cu' (Fun Ap [t⇩1, t⇩2]) n"
abbreviation is_Cu where "is_Cu t ≡ is_Cu' t 0"
lemma is_Cu_intro:
assumes "funas_term t ⊆ ℱ"
shows "is_Cu (Cu t)"
using assms
proof (induction t)
case (Fun f ts)
hence props: "Some (length ts) = sigF f" "∀t'∈set ts. funas_term t' ⊆ ℱ"
using ℱ_def by auto
hence "f ≠ Ap" using fresh by force
{ fix m
assume "Some (length ts + m) = sigF f"
moreover have "t' ∈ set ts ⟶ is_Cu (Cu t')" for t' using Fun by auto
ultimately have "is_Cu' (Cu (Fun f ts)) m" using props(2)
proof (induction "length ts" arbitrary: ts m)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have "Cu (Fun f ts) = Fun Ap [Cu (Fun f ts'), Cu a]"
using ‹f ≠ Ap› unfolding ts_def by simp
have "is_Cu (Cu a)" using Suc(4) unfolding ts_def by auto
moreover have "is_Cu' (Cu (Fun f ts')) (Suc m)"
using Suc(1)[of ts' "Suc m"] Suc(2-) unfolding ts_def by auto
ultimately show ?case using ‹f ≠ Ap› unfolding ts_def by auto
qed auto
}
thus ?case using props(1) by fastforce
qed auto
lemma is_Cu_elim':
assumes "is_Cu' t n"
shows "(∃f ts. Some (length ts + n) = sigF f ∧
(∀t' ∈ set ts. funas_term t' ⊆ ℱ) ∧ t = Cu (Fun f ts))
∨ n = 0 ∧ (∃x. t = Var x)"
using assms
proof (induction t n rule: is_Cu'.induct)
case (funs f m)
hence "Some (length [] + m) = sigF f ∧ (∀t'∈set []. funas_term t' ⊆ ℱ) ∧
Fun f [] = Cu (Fun f [])" using arity_def by simp
thus ?case by blast
next
case (ap t⇩1 n t⇩2)
then obtain f ts' where inner: "Some (length ts' + Suc n) = sigF f ∧
(∀t' ∈ set ts'. funas_term t' ⊆ ℱ) ∧ t⇩1 = Cu (Fun f ts')" by blast
hence "f ≠ Ap" using fresh by force
obtain g ss where t⇩2'_props: "Some (length ss) = sigF g ∧
(∀t'∈set ss. funas_term t' ⊆ ℱ) ∧ t⇩2 = Cu (Fun g ss) ∨ (∃x. t⇩2 = Var x)"
using ap(4) by auto
thus ?case
proof (elim disjE)
assume t⇩2_props: "Some (length ss) = sigF g ∧
(∀t'∈set ss. funas_term t' ⊆ ℱ) ∧ t⇩2 = Cu (Fun g ss)"
let ?ts = "ts' @ [Fun g ss]"
have "Some (length ?ts + n) = sigF f ∧
(∀t' ∈ set ?ts. funas_term t' ⊆ ℱ) ∧ Fun Ap [t⇩1, t⇩2] = Cu (Fun f ?ts)"
using inner t⇩2_props ‹f ≠ Ap› ℱ_def by auto
thus ?thesis by blast
next
assume "∃x. t⇩2 = Var x"
then obtain x where t⇩2_def: "t⇩2 = Var x" by blast
let ?ts = "ts' @ [Var x]"
have "Some (length ?ts + n) = sigF f ∧
(∀t' ∈ set ?ts. funas_term t' ⊆ ℱ) ∧ Fun Ap [t⇩1, t⇩2] = Cu (Fun f ?ts)"
using inner t⇩2_def ‹f ≠ Ap› by auto
thus ?thesis by blast
qed
qed blast
lemma is_Cu_elim:
assumes "is_Cu' t 0"
shows "∃t'. funas_term t' ⊆ ℱ ∧ t = Cu t'"
proof (cases t)
case (Var x)
thus ?thesis by (auto intro: exI[of _ "Var x"])
next
case (Fun f ts)
then obtain f' ts' where props: "Some (length ts' + 0) = sigF f' ∧
(∀t'∈set ts'. funas_term t' ⊆ ℱ) ∧ t = Cu (Fun f' ts')"
using is_Cu_elim'[OF assms] by blast
hence "funas_term (Fun f' ts') ⊆ ℱ ∧ t = Cu (Fun f' ts')" unfolding ℱ_def by auto
thus ?thesis by blast
qed
lemma Cu'_subst_Cu':
assumes "is_Cu' t n" "∀x. x ∈ vars_term t ⟶ is_Cu (Var x ⋅ σ)"
shows "is_Cu' (t ⋅ σ) n"
using assms by (induction rule: is_Cu'.induct) auto
lemma Cu_subst_Cu:
assumes "is_Cu t" "∀x. x ∈ vars_term t ⟶ is_Cu (Var x ⋅ σ)"
shows "is_Cu (t ⋅ σ)"
using assms Cu'_subst_Cu' by blast
lemma is_Cu'_unique:
assumes "is_Cu' t n" "is_Cu' t m"
shows "n = m"
using assms
by (induction t n arbitrary: m rule: is_Cu'.induct) (force elim: is_Cu'.cases)+
lemma replace_in_Cu:
assumes "is_Cu' C⟨s'⟩ n" "is_Cu s'" "is_Cu t'"
shows "is_Cu' C⟨t'⟩ n"
using assms
proof (induction C arbitrary: n)
case Hole
hence "n = 0" using is_Cu'_unique by force
thus ?case using Hole by simp
next
case (More f ss1 C' ss2)
hence "f = Ap" by (auto elim: is_Cu'.cases)
consider "∃a. ss1 = [] ∧ ss2 = [a]" | "∃a. ss2 = [] ∧ ss1 = [a]"
using More(2) by (cases ss1; cases ss2) (auto elim: is_Cu'.cases)
thus ?case
proof cases
case 1
thus ?thesis using More by (auto elim: is_Cu'.cases)
next
case 2
then obtain a where lists: "ss2 = [] ∧ ss1 = [a]" by blast
hence "is_Cu' a (Suc n)" "is_Cu C'⟨t'⟩" using More by (auto elim: is_Cu'.cases)
thus ?thesis using lists ‹f = Ap› by auto
qed
qed
lemma vars_term_subst_Cu:
assumes "is_Cu' t n" "is_Cu' (t ⋅ σ) n"
shows "∀x ∈ vars_term t. is_Cu (Var x ⋅ σ)"
using assms by (induction rule: is_Cu'.induct) (auto elim: is_Cu'.cases)
lemma nothing_missing_lhs_Cu⇩R:
assumes "r ∈ Cu⇩R ℛ"
shows "missing_args (mctxt_of_term (fst r ⋅ σ)) 0 = 1"
proof -
obtain l' r' where lhs_rhs_def: "fst r = Cu l'" "snd r = Cu r'" "(l', r') ∈ ℛ"
using assms(1) Cu⇩R_def by auto
moreover have "is_Fun l'"
using ‹(l', r') ∈ ℛ› wfR unfolding wf_trs_def by blast
ultimately have "missing_args (mctxt_of_term (l' ⋅ σ)) 0 = 1"
using nothing_missing_lhs_ℛ by force
hence "missing_args (mctxt_of_term ((Cu l') ⋅ σ)) 0 = 1"
using missing_persists_Cu[of l' σ] unfolding missing_args_unfold[symmetric]
by (cases "is_Fun l'") auto
thus ?thesis using lhs_rhs_def by argo
qed
lemma is_Cu_Cu⇩R:
assumes "(l, r) ∈ Cu⇩R ℛ"
shows "is_Cu l" "is_Cu r"
proof -
obtain l' r' where lr_def: "l = Cu l'" "r = Cu r'" "(l', r') ∈ ℛ"
using assms unfolding Cu⇩R_def by blast
moreover have "funas_term l' ⊆ ℱ" "funas_term r' ⊆ ℱ"
using lr_def(3) sigR ℱ_def
unfolding funas_trs_def funas_rule_def by force+
ultimately show "is_Cu l" "is_Cu r" using is_Cu_intro by simp+
qed
lemma is_Cu'_n0:
assumes "missing_args (mctxt_of_term t) n = 1"
shows "is_Cu' t m ⟶ m = n"
using assms
proof (induction "mctxt_of_term t" n arbitrary: t m rule: missing_args.induct)
case (2 x n)
then show ?case by (cases t) auto
next
case (3 f Cs n)
then obtain ts where t_def: "t = Fun f ts" "Cs = map mctxt_of_term ts" by (cases t) simp+
thus ?case
proof (cases "f = Ap ∧ length Cs = 2")
case True
then obtain "is_Cu' (ts ! 0) (Suc m) ⟶ Suc m = Suc n"
using 3(1)[OF True, of "ts ! 0" "Suc m"] 3(3) unfolding t_def by auto
thus ?thesis using True unfolding t_def by (auto elim: is_Cu'.cases)
next
case False
thus ?thesis using 3(2-) unfolding t_def by (auto elim: is_Cu'.cases simp: arity_def)
qed
qed simp
lemma Cu_subst_in_ctxt:
assumes "is_Cu' C⟨l ⋅ σ⟩ n" "is_Cu l" "is_Fun l" "missing_args (mctxt_of_term (l ⋅ σ)) 0 = 1"
shows "C ≠ □ ⟶ is_Cu (l ⋅ σ)"
using assms(1,4)
proof (induction C arbitrary: n)
case (More f ss1 C' ss2)
consider "∃a. ss1 = [] ∧ ss2 = [a]" | "∃a. ss2 = [] ∧ ss1 = [a]"
using More(2) by (cases ss1; cases ss2) (auto elim: is_Cu'.cases)
thus ?case
proof cases
case 1
thus ?thesis using More is_Cu'_n0[OF More(3)] by (cases C') (auto elim: is_Cu'.cases)
next
case 2
then obtain a where lists: "ss2 = [] ∧ ss1 = [a]" by blast
hence "is_Cu' a (Suc n)" "is_Cu C'⟨l ⋅ σ⟩" using More by (auto elim: is_Cu'.cases)
thus ?thesis using lists More by (cases C') auto
qed
qed blast
lemma Cu_step_persists:
assumes "(s, t) ∈ rstep (Cu⇩R ℛ)" "is_Cu s"
shows "is_Cu t"
proof -
obtain l r p σ where step: "(s, t) ∈ rstep_r_p_s (Cu⇩R ℛ) (l, r) p σ"
using rstep_iff_rstep_r_p_s[of _ _ "Cu⇩R ℛ"] assms(1) by blast
obtain C where props: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "p = hole_pos C" "(l, r) ∈ Cu⇩R ℛ"
using hole_pos_ctxt_of_pos_term[of p s]
Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
unfolding fst_conv snd_conv by metis
hence nothing_missing: "missing_args (mctxt_of_term (l ⋅ σ)) 0 = 1"
using nothing_missing_lhs_Cu⇩R by force
have "is_Cu l" "is_Cu r" using is_Cu_Cu⇩R[OF props(4)] by simp+
hence "is_Cu (l ⋅ σ)"
using Cu_subst_in_ctxt[OF _ _ _ nothing_missing] assms(2) wf_Cu props(4)
unfolding props(1) wf_trs_def by (cases C) (simp, blast)
hence is_Cu_σl: "∀x. x ∈ vars_term l ⟶ is_Cu (Var x ⋅ σ)"
using vars_term_subst_Cu ‹is_Cu l› by blast
hence is_Cu_σr: "∀x. x ∈ vars_term r ⟶ is_Cu (Var x ⋅ σ)"
using wf_Cu props(4) unfolding wf_trs_def by blast
have "is_Cu (r ⋅ σ)"
using Cu_subst_Cu[OF ‹is_Cu r› is_Cu_σr] .
thus ?thesis using replace_in_Cu[OF _ ‹is_Cu (l ⋅ σ)› ‹is_Cu (r ⋅ σ)›, of C]
props(1,2) assms(2) by blast
qed
lemma Cu_eq_NF_𝒰_eq':
assumes "Cu s = Cu t" "funas_term s ⊆ ℱ"
shows "NF_𝒰 (Cu t) = s"
using assms(1) NF_𝒰_Cu[OF assms(2)] by simp
lemma Cu⇩R_NF_𝒰_ℛ_steps:
assumes "(Cu s, Cu t) ∈ (rstep (Cu⇩R ℛ))⇧*" "funas_term s ⊆ ℱ"
shows "(s, NF_𝒰 (Cu t)) ∈ (rstep ℛ)⇧*"
proof -
show ?thesis using assms
proof (induction "Cu s" arbitrary: s rule: converse_rtrancl_induct)
case base
thus ?case using Cu_eq_NF_𝒰_eq'[of s t] by simp
next
case (step z)
have "is_Cu (Cu s)" using is_Cu_intro[OF step(4)] .
then obtain z' where is_Cu_z: "funas_term z' ⊆ ℱ ∧ z = Cu z'"
using is_Cu_elim[OF Cu_step_persists[OF step(1)]] by blast
hence "(s, z') ∈ (rstep ℛ)⇧*"
using Cu⇩R_NF_𝒰_ℛ_step[of s z'] step(1,4) by fastforce
thus ?case using step(3)[of z'] is_Cu_z by fastforce
qed
qed
theorem main_result_sound:
assumes "CR (rstep (Cu⇩R ℛ))"
shows "CR (rstep ℛ)"
proof -
{ fix a :: "('f, 'v) term"
assume funas_a: "funas_term a ⊆ ℱ"
{ fix b c
assume peak: "(a, b) ∈ (rstep ℛ)⇧*" "(a, c) ∈ (rstep ℛ)⇧*"
hence funas: "funas_term b ⊆ ℱ" "funas_term c ⊆ ℱ"
using rsteps_preserve_funas_terms[OF sigR funas_a[unfolded ℱ_def] _ wfR]
unfolding ℱ_def by blast+
hence NF_𝒰_Cu_bc: "NF_𝒰 (Cu b) = b" "NF_𝒰 (Cu c) = c" using NF_𝒰_Cu by auto
have "(Cu a, Cu b) ∈ (rstep (Cu⇩R ℛ))⇧*" "(Cu a, Cu c) ∈ (rstep (Cu⇩R ℛ))⇧*"
using peak rtrancl_map[OF g_prop1, of "rstep ℛ" id a] unfolding rtrancl_idemp by auto
then obtain d' where join: "(Cu b, d') ∈ (rstep (Cu⇩R ℛ))⇧* ∧ (Cu c, d') ∈ (rstep (Cu⇩R ℛ))⇧*"
using assms unfolding CR_defs by blast
hence "d' ∈ 𝒯⇩C⇩u" using funas_Cu[OF funas(1)]
by simp (meson funas_Cu⇩R rsteps_preserve_funas_terms wf_Cu)
hence "Cu d' = d'" using 𝒯⇩C⇩u_Cu_eq by blast
have "(b, NF_𝒰 d') ∈ (rstep ℛ)⇧* ∧ (c, NF_𝒰 d') ∈ (rstep ℛ)⇧*"
using Cu⇩R_NF_𝒰_ℛ_steps[OF _ funas(1), of d'] Cu⇩R_NF_𝒰_ℛ_steps[OF _ funas(2), of d'] join
unfolding ‹Cu d' = d'› by blast
hence "(b, c) ∈ (rstep ℛ)⇧↓" by blast
}
hence "CR_on (rstep ℛ) {a}" unfolding CR_defs by simp
}
hence "CR_on (rstep ℛ) { t. funas_term t ⊆ ℱ }" unfolding CR_on_def by auto
thus ?thesis using CR_on_imp_CR[OF wfR sigR] unfolding ℱ_def by blast
qed
end
end