theory MyhillNerode

  imports "Main" "List_Prefix"

begin

text {* sequential composition of languages *}

definition

  Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

where 

  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

inductive_set

  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

  for L :: "string set"

where

  start[intro]: "[] \<in> L\<star>"

| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 

theorem ardens_revised:

  assumes nemp: "[] \<notin> A"

  shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"

proof

  assume eq: "X = B ;; A\<star>"

  have "A\<star> =  {[]} \<union> A\<star> ;; A" sorry

  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp

  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  unfolding Seq_def by auto

  also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"  unfolding Seq_def

    by (auto) (metis append_assoc)+

  finally show "X = X ;; A \<union> B" using eq by auto

next

  assume "X = X ;; A \<union> B"

  then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto

  show "X = B ;; A\<star>" sorry

qed

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

consts L:: "'a \<Rightarrow> string set"

overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"

begin

fun

  L_rexp :: "rexp \<Rightarrow> string set"

where

    "L_rexp (NULL) = {}"

  | "L_rexp (EMPTY) = {[]}"

  | "L_rexp (CHAR c) = {[c]}"

  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"

  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

  | "L_rexp (STAR r) = (L_rexp r)\<star>"

end

definition 

  folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"

where

  "folds f z S \<equiv> SOME x. fold_graph f z S x"

lemma folds_simp_null [simp]:

  "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> L r)"

apply (simp add: folds_def)

apply (rule someI2_ex)

apply (erule finite_imp_fold_graph)

apply (erule fold_graph.induct)

apply (auto)

done

lemma [simp]:

  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"

by simp

definition

  str_eq ("_ \<approx>_ _")

where

  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"

definition

  str_eq_rel ("\<approx>_")

where

  "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"

section {* finite \<Rightarrow> regular *}

definition

  transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")

where

  "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"

definition

  transitions_rexp ("_ \<turnstile>\<rightarrow> _")

where

  "Y \<turnstile>\<rightarrow> X \<equiv> folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"

definition

  "init_rhs CS X \<equiv> if X = {[]} 

                   then {({[]}, EMPTY)} 

                   else if ([] \<in> X)

                        then insert ({[]}, EMPTY) {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}

                        else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"

overloading L_rhs \<equiv> "L:: (string set \<times> rexp) set \<Rightarrow> string set"

begin

fun L_rhs:: "(string set \<times> rexp) set \<Rightarrow> string set"

where

  "L_rhs rhs = \<Union> {(Y;; L r) | Y r . (Y, r) \<in> rhs}"

end

definition

  "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, init_rhs CS X)})"

lemma [simp]:

  shows "finite (Y \<Turnstile>\<Rightarrow> X)"

unfolding transitions_def

by auto

lemma defined_by_str:

  assumes "s \<in> X" 

  and "X \<in> UNIV // (\<approx>Lang)"

  shows "X = (\<approx>Lang) `` {s}"

using assms

unfolding quotient_def Image_def

unfolding str_eq_rel_def str_eq_def

by auto

(************ arden's lemma variation ********************)

definition 

  "rexp_of rhs X \<equiv> folds ALT NULL {r. (X, r) \<in> rhs}"

definition 

  "arden_variate X rhs \<equiv> {(Y, SEQ r (STAR (rexp_of rhs X)))| Y r. (Y, r) \<in> rhs \<and> Y \<noteq> X}"

(************* rhs/equations property **************)

definition 

  "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"

(*********** substitution of ES *************)

text {* rhs_subst rhs X xrhs: substitude all occurence of X in rhs with xrhs *}

definition 

  "rhs_subst rhs X xrhs \<equiv> {(Y, r) | Y r. Y \<noteq> X \<and> (Y, r) \<in> rhs} \<union> 

                          {(X, SEQ r\<^isub>1 r\<^isub>2 ) | r\<^isub>1 r\<^isub>2. (X, r\<^isub>1) \<in> xrhs \<and> (X, r\<^isub>2) \<in> rhs}"

definition

  "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"

text {*

  Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds.

*}

definition 

  "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> ([] \<notin> L (rexp_of rhs X)) \<and> X = L rhs"

definition 

  "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"

definition 

  "self_contained ES \<equiv> \<forall> X xrhs. (X, xrhs) \<in> ES 

                             \<longrightarrow> (\<forall> Y r.(Y, r) \<in> xrhs \<and> Y \<noteq> {[]} \<longrightarrow> (\<exists> yrhs. (Y, yrhs) \<in> ES))"

definition 

  "Inv ES \<equiv> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> non_empty ES \<and> self_contained ES"

lemma wf_iter [rule_format]: 

  fixes f

  assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"

  shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"

proof(induct e rule: wf_induct 

           [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify)

  fix x 

  assume h [rule_format]: 

    "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')"

    and px: "P x"

  show "\<exists>e'. P e' \<and> Q e'"

  proof(cases "Q x")

    assume "Q x" with px show ?thesis by blast

  next

    assume nq: "\<not> Q x"

    from step [OF px nq]

    obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto

    show ?thesis

    proof(rule h)

      from ltf show "(e', x) \<in> inv_image less_than f" 

	by (simp add:inv_image_def)

    next

      from pe' show "P e'" .

    qed

  qed

qed

text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *}

lemma init_ES_satisfy_Inv:

  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"

  and X_in_eq_cls: "X \<in> (UNIV // (\<approx>Lang))"

  shows "Inv (eqs (UNIV // (\<approx>Lang)))"

proof -

  have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS

    by (auto simp add:eqs_def)

  moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     

    by (auto simp:distinct_equas_def eqs_def)

  moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"

  proof-

    have "\<And> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<Longrightarrow> ([] \<notin> L (rexp_of rhs X))"

    proof 

      apply (auto simp:eqs_def rexp_of_def)

      sorry

    moreover have "\<forall> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<longrightarrow> X = L rhs"

      sorry

    ultimately show ?thesis by (simp add:ardenable_def)

  qed

  moreover have "non_empty (eqs (UNIV // (\<approx>Lang)))"

    by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def str_eq_def)

  moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"

    by (auto simp:self_contained_def eqs_def init_rhs_def)

  ultimately show ?thesis by (simp add:Inv_def)

qed

text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}

lemma iteration_step: 

  assumes Inv_ES: "Inv ES"

  and    X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"

  and    not_T: "card ES > 1"

  shows "(\<exists> ES' xrhs'. Inv ES' \<and> (card ES', card ES) \<in> less_than \<and> (X, xrhs') \<in> ES')" 

proof -

lemma distinct_rhs_equations:

  "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"

by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters)

lemma every_nonempty_eqclass_has_strings:

  "\<lbrakk>X \<in> (UNIV Quo Lang); X \<noteq> {[]}\<rbrakk> \<Longrightarrow> \<exists> clist. clist \<in> X \<and> clist \<noteq> []"

by (auto simp:quot_def equiv_class_def equiv_str_def)

lemma every_eqclass_is_derived_from_empty:

  assumes not_empty: "X \<noteq> {[]}"

  shows "X \<in> (UNIV Quo Lang) \<Longrightarrow> \<exists> clist. {[]};{clist} \<subseteq> X \<and> clist \<noteq> []"

using not_empty

apply (drule_tac every_nonempty_eqclass_has_strings, simp)

by (auto intro:exI[where x = clist] simp:lang_seq_def)

lemma equiv_str_in_CS:

  "\<lbrakk>clist\<rbrakk>Lang \<in> (UNIV Quo Lang)"

by (auto simp:quot_def)

lemma has_str_imp_defined_by_str:

  "\<lbrakk>str \<in> X; X \<in> UNIV Quo Lang\<rbrakk> \<Longrightarrow> X = \<lbrakk>str\<rbrakk>Lang"

by (auto simp:quot_def equiv_class_def equiv_str_def)

lemma every_eqclass_has_ascendent:

  assumes has_str: "clist @ [c] \<in> X"

  and     in_CS:   "X \<in> UNIV Quo Lang"

  shows "\<exists> Y. Y \<in> UNIV Quo Lang \<and> Y-c\<rightarrow>X \<and> clist \<in> Y" (is "\<exists> Y. ?P Y")

proof -

  have "?P (\<lbrakk>clist\<rbrakk>Lang)" 

  proof -

    have "\<lbrakk>clist\<rbrakk>Lang \<in> UNIV Quo Lang"       

      by (simp add:quot_def, rule_tac x = clist in exI, simp)

    moreover have "\<lbrakk>clist\<rbrakk>Lang-c\<rightarrow>X" 

    proof -

      have "X = \<lbrakk>(clist @ [c])\<rbrakk>Lang" using has_str in_CS

        by (auto intro!:has_str_imp_defined_by_str)

      moreover have "\<forall> sl. sl \<in> \<lbrakk>clist\<rbrakk>Lang \<longrightarrow> sl @ [c] \<in> \<lbrakk>(clist @ [c])\<rbrakk>Lang"

        by (auto simp:equiv_class_def equiv_str_def)

      ultimately show ?thesis unfolding CT_def lang_seq_def

        by auto

    qed

    moreover have "clist \<in> \<lbrakk>clist\<rbrakk>Lang" 

      by (auto simp:equiv_str_def equiv_class_def)

    ultimately show "?P (\<lbrakk>clist\<rbrakk>Lang)" by simp

  qed

  thus ?thesis by blast

qed

lemma finite_charset_rS:

  "finite {CHAR c |c. Y-c\<rightarrow>X}"

by (rule_tac A = UNIV and f = CHAR in finite_surj, auto)

lemma l_eq_r_in_equations:

  assumes X_in_equas: "(X, xrhs) \<in> equations (UNIV Quo Lang)"

  shows "X = L xrhs"    

proof (cases "X = {[]}")

  case True

  thus ?thesis using X_in_equas 

    by (simp add:equations_def equation_rhs_def lang_seq_def)

next

  case False 

  show ?thesis

  proof 

    show "X \<subseteq> L xrhs"

    proof

      fix x

      assume "(1)": "x \<in> X"

      show "x \<in> L xrhs"          

      proof (cases "x = []")

        assume empty: "x = []"

        hence "x \<in> L (empty_rhs X)" using "(1)"

          by (auto simp:empty_rhs_def lang_seq_def)

        thus ?thesis using X_in_equas False empty "(1)" 

          unfolding equations_def equation_rhs_def by auto

      next

        assume not_empty: "x \<noteq> []"

        hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto)

        then obtain clist c where decom: "x = clist @ [c]" by blast

        moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>

          \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

        proof -

          fix Y

          assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"

            and Y_CT_X: "Y-c\<rightarrow>X"

            and clist_in_Y: "clist \<in> Y"

          with finite_charset_rS 

          show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

            by (auto simp :fold_alt_null_eqs)

        qed

        hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" 

          using X_in_equas False not_empty "(1)" decom

          by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def)

        then obtain Xa where 

          "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast

        hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" 

          using X_in_equas "(1)" decom

          by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])

        thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def

          by auto

      qed

    qed

  next

    show "L xrhs \<subseteq> X"

    proof

      fix x 

      assume "(2)": "x \<in> L xrhs"

      have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

        using finite_charset_rS

        by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)

      have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

        by (simp add:empty_rhs_def split:if_splits)

      show "x \<in> X" using X_in_equas False "(2)"         

        by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)

    qed

  qed

qed

lemma no_EMPTY_equations:

  "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"

apply (clarsimp simp add:equations_def equation_rhs_def)

apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)

apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+

done

lemma init_ES_satisfy_ardenable:

  "(X, xrhs) \<in> equations (UNIV Quo Lang)  \<Longrightarrow> ardenable (X, xrhs)"  

  unfolding ardenable_def

  by (auto intro:distinct_rhs_equations no_EMPTY_equations simp:l_eq_r_in_equations simp del:L_rhs.simps)

lemma init_ES_satisfy_Inv:

  assumes finite_CS: "finite (UNIV Quo Lang)"

  and X_in_eq_cls: "X \<in> UNIV Quo Lang"

  shows "Inv X (equations (UNIV Quo Lang))"

proof -

  have "finite (equations (UNIV Quo Lang))" using finite_CS

    by (auto simp:equations_def)    

  moreover have "\<exists>rhs. (X, rhs) \<in> equations (UNIV Quo Lang)" using X_in_eq_cls 

    by (simp add:equations_def)

  moreover have "distinct_equas (equations (UNIV Quo Lang))" 

    by (auto simp:distinct_equas_def equations_def)

  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow>

                 rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equations (UNIV Quo Lang)))" 

    apply (simp add:left_eq_cls_def equations_def rhs_eq_cls_def equation_rhs_def)

    by (auto simp:empty_rhs_def split:if_splits)

  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> X \<noteq> {}"

    by (clarsimp simp:equations_def empty_notin_CS intro:classical)

  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> ardenable (X, xrhs)"

    by (auto intro!:init_ES_satisfy_ardenable)

  ultimately show ?thesis by (simp add:Inv_def)

qed

text {* *********** END: proving the initial equation-system satisfies Inv ******* *}

text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}

lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>

       \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "

apply (case_tac "insert a A = {a}")

by (auto simp:TCon_def)

lemma not_T_atleast_2[rule_format]:

  "finite S \<Longrightarrow> \<forall> x. x \<in> S \<and> (\<not> TCon S)\<longrightarrow> (\<exists> y. x \<noteq> y \<and> y \<in> S)"

apply (erule finite.induct, simp)

apply (clarify, case_tac "x = a")

by (erule not_T_aux, auto)

lemma exist_another_equa: 

  "\<lbrakk>\<not> TCon ES; finite ES; distinct_equas ES; (X, rhl) \<in> ES\<rbrakk> \<Longrightarrow> \<exists> Y yrhl. (Y, yrhl) \<in> ES \<and> X \<noteq> Y"

apply (drule not_T_atleast_2, simp)

apply (clarsimp simp:distinct_equas_def)

apply (drule_tac x= X in spec, drule_tac x = rhl in spec, drule_tac x = b in spec)

by auto

lemma Inv_mono_with_lambda:

  assumes Inv_ES: "Inv X ES"

  and X_noteq_Y:  "X \<noteq> {[]}"

  shows "Inv X (ES - {({[]}, yrhs)})"

proof -

  have "finite (ES - {({[]}, yrhs)})" using Inv_ES

    by (simp add:Inv_def)

  moreover have "\<exists>rhs. (X, rhs) \<in> ES - {({[]}, yrhs)}" using Inv_ES X_noteq_Y

    by (simp add:Inv_def)

  moreover have "distinct_equas (ES - {({[]}, yrhs)})" using Inv_ES X_noteq_Y

    apply (clarsimp simp:Inv_def distinct_equas_def)

    by (drule_tac x = Xa in spec, simp)    

  moreover have "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

                          ardenable (X, xrhs) \<and> X \<noteq> {}" using Inv_ES

    by (clarify, simp add:Inv_def)

  moreover 

  have "insert {[]} (left_eq_cls (ES - {({[]}, yrhs)})) = insert {[]} (left_eq_cls ES)"

    by (auto simp:left_eq_cls_def)

  hence "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

                          rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (ES - {({[]}, yrhs)}))"

    using Inv_ES by (auto simp:Inv_def)

  ultimately show ?thesis by (simp add:Inv_def)

qed

lemma non_empty_card_prop:

  "finite ES \<Longrightarrow> \<forall>e. e \<in> ES \<longrightarrow> card ES - Suc 0 < card ES"

apply (erule finite.induct, simp)

apply (case_tac[!] "a \<in> A")

by (auto simp:insert_absorb)

lemma ardenable_prop:

  assumes not_lambda: "Y \<noteq> {[]}"

  and ardable: "ardenable (Y, yrhs)"

  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")

proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")

  case True

  thus ?thesis 

  proof 

    fix reg

    assume self_contained: "(Y, reg) \<in> yrhs"

    show ?thesis 

    proof -

      have "?P (arden_variate Y reg yrhs)"

      proof -

        have "Y = L (arden_variate Y reg yrhs)" 

          using self_contained not_lambda ardable

          by (rule_tac arden_variate_valid, simp_all add:ardenable_def)

        moreover have "distinct_rhs (arden_variate Y reg yrhs)" 

          using ardable 

          by (auto simp:distinct_rhs_def arden_variate_def seq_rhs_r_def del_x_paired_def ardenable_def)

        moreover have "rhs_eq_cls (arden_variate Y reg yrhs) = rhs_eq_cls yrhs - {Y}"

        proof -

          have "\<And> rhs r. rhs_eq_cls (seq_rhs_r rhs r) = rhs_eq_cls rhs"

            apply (auto simp:rhs_eq_cls_def seq_rhs_r_def image_def)

            by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "(x, ra)" in bexI, simp+)

          moreover have "\<And> rhs X. rhs_eq_cls (del_x_paired rhs X) = rhs_eq_cls rhs - {X}"

            by (auto simp:rhs_eq_cls_def del_x_paired_def)

          ultimately show ?thesis by (simp add:arden_variate_def)

        qed

        ultimately show ?thesis by simp

      qed

      thus ?thesis by (rule_tac x= "arden_variate Y reg yrhs" in exI, simp)

    qed

  qed

next

  case False