1 (* CR_Takahashi from Nominal1 ported to Nominal2 *)

     2 theory CR 

     3 imports "../Nominal2" 

     4 begin

     5 

     6 atom_decl name

     7 

     8 nominal_datatype lam =

     9   Var "name"

    10 | App "lam" "lam"

    11 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

    12 

    13 nominal_primrec

    14   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)

    15 where

    16   "(Var x)[y ::= s] = (if x = y then s else (Var x))"

    17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

    18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

    19   unfolding eqvt_def subst_graph_def

    20   apply (rule, perm_simp, rule)

    21   apply(rule TrueI)

    22   apply(auto)

    23   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

    24   apply(blast)+

    25   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    26   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    27   apply(simp_all add: Abs_fresh_iff)

    28   apply(simp add: fresh_star_def fresh_Pair)

    29   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    30   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    31   done

    32 

    33 termination (eqvt)

    34   by lexicographic_order

    35 

    36 lemma forget:

    37   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

    38   by (nominal_induct t avoiding: x s rule: lam.strong_induct)

    39      (auto simp add: lam.fresh fresh_at_base)

    40 

    41 lemma fresh_fact:

    42   fixes z::"name"

    43   assumes a: "atom z \<sharp> s"

    44       and b: "z = y \<or> atom z \<sharp> t"

    45   shows "atom z \<sharp> t[y ::= s]"

    46   using a b

    47   by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

    48      (auto simp add: lam.fresh fresh_at_base)

    49 

    50 lemma substitution_lemma:

    51   assumes a: "x \<noteq> y" "atom x \<sharp> u"

    52   shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"

    53   using a

    54   by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)

    55      (auto simp add: fresh_fact forget)

    56 

    57 lemma subst_rename:

    58   assumes a: "atom y \<sharp> t"

    59   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"

    60   using a

    61   by (nominal_induct t avoiding: x y s rule: lam.strong_induct)

    62      (auto simp add: lam.fresh fresh_at_base)

    63 

    64 lemma supp_subst:

    65   shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"

    66   by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)

    67 

    68 inductive

    69   beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)

    70 where

    71   b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"

    72 | b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"

    73 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"

    74 | b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"

    75 

    76 equivariance beta

    77 

    78 nominal_inductive beta

    79   avoids b3: x

    80        | b4: x

    81   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

    82 

    83 section {* Transitive Closure of Beta *}

    84 

    85 inductive

    86   beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80)

    87 where

    88   bs1[intro, simp]: "M \<longrightarrow>b* M"

    89 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"

    90 

    91 equivariance beta_star

    92 

    93 lemma bs3[intro, trans]:

    94   assumes "A \<longrightarrow>b* B"

    95   and     "B \<longrightarrow>b* C"

    96   shows   "A \<longrightarrow>b* C"

    97   using assms(2) assms(1)

    98   by induct auto

    99 

   100 section {* One-Reduction *}

   101 

   102 inductive

   103   One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)

   104 where

   105   o1[intro]: "Var x \<longrightarrow>1 Var x"

   106 | o2[intro]: "\<lbrakk>t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>1 App t2 s2"

   107 | o3[intro]: "t1 \<longrightarrow>1 t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>1 Lam [x].t2"

   108 | o4[intro]: "\<lbrakk>atom x \<sharp> (s1, s2); t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]"

   109 

   110 equivariance One

   111 

   112 nominal_inductive One

   113   avoids o3: "x"

   114       |  o4: "x"

   115   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

   116 

   117 lemma One_refl:

   118   shows "t \<longrightarrow>1 t"

   119   by (nominal_induct t rule: lam.strong_induct) (auto)

   120 

   121 lemma One_subst:

   122   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"

   123   shows "t1[x ::= s1] \<longrightarrow>1 t2[x ::= s2]"

   124   using a

   125   by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)

   126      (auto simp add: substitution_lemma fresh_at_base fresh_fact fresh_Pair)

   127 

   128 lemma better_o4_intro:

   129   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"

   130   shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"

   131 proof -

   132   obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh)

   133   have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs

   134     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)

   135   also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)

   136   also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])

   137   finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp

   138 qed

   139 

   140 lemma One_Var:

   141   assumes a: "Var x \<longrightarrow>1 M"

   142   shows "M = Var x"

   143   using a by (cases rule: One.cases) (simp_all)

   144 

   145 lemma One_Lam:

   146   assumes a: "Lam [x].t \<longrightarrow>1 s" "atom x \<sharp> s"

   147   shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>1 t'"

   148   using a

   149   apply (cases rule: One.cases)

   150   apply (auto simp add: Abs1_eq_iff)

   151   apply (rule_tac x="(atom xa \<rightleftharpoons> atom x) \<bullet> t2" in exI)

   152   apply (auto simp add: fresh_permute_left lam.fresh)

   153   by (metis swap_commute One.eqvt)

   154 

   155 lemma One_App:

   156   assumes a: "App t s \<longrightarrow>1 r"

   157   shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>1 t' \<and> s \<longrightarrow>1 s') \<or>

   158          (\<exists>x p p' s'. r = p'[x ::= s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>1 p' \<and> s \<longrightarrow>1 s' \<and> atom x \<sharp> (s,s'))"

   159   using a by (cases rule: One.cases) auto

   160 

   161 lemma One_preserves_fresh:

   162   fixes x::"name"

   163   assumes a: "M \<longrightarrow>1 N"

   164   shows "atom x \<sharp> M \<Longrightarrow> atom x \<sharp> N"

   165   using a

   166   by (induct, auto simp add: lam.fresh)

   167      (metis fresh_fact)+

   168 

   169 (* TODO *)

   170 lemma One_strong_cases[consumes 1]:

   171   "\<lbrakk> a1 \<longrightarrow>1 a2; \<And>x. \<lbrakk>a1 = Var x; a2 = Var x\<rbrakk> \<Longrightarrow> P;

   172  \<And>t1 t2 s1 s2. \<lbrakk>a1 = App t1 s1; a2 = App t2 s2;  t1 \<longrightarrow>1 t2;  s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> P;

   173  \<And>t1 t2. (\<lbrakk>atom xa \<sharp> a1; atom xa \<sharp> a2\<rbrakk> \<Longrightarrow> a1 = Lam [xa].t1 \<and> a2 = Lam [xa].t2 \<and>  t1 \<longrightarrow>1 t2) \<Longrightarrow> P;

   174  \<And>s1 s2 t1 t2.

   175     (\<lbrakk>atom xaa \<sharp> a1; atom xaa \<sharp> a2\<rbrakk>

   176      \<Longrightarrow> a1 = App (Lam [xaa].t1) s1 \<and> a2 = t2[xaa::=s2] \<and> atom xaa \<sharp> (s1, s2) \<and>  t1 \<longrightarrow>1 t2 \<and>  s1 \<longrightarrow>1 s2) \<Longrightarrow>

   177     P\<rbrakk>

   178   \<Longrightarrow> P"

   179   apply (nominal_induct avoiding: a1 a2 rule: One.strong_induct)

   180   apply blast

   181   apply blast

   182   apply (simp add: fresh_Pair_elim Abs1_eq_iff lam.fresh)

   183   apply (case_tac "xa = x")

   184   apply (simp_all)[2]

   185   apply blast

   186   apply (rotate_tac 6)

   187   apply (drule_tac x="(atom x \<rightleftharpoons> atom xa) \<bullet> t1" in meta_spec)

   188   apply (rotate_tac -1)

   189   apply (drule_tac x="(atom x \<rightleftharpoons> atom xa) \<bullet> t2" in meta_spec)

   190   apply (simp add: One.eqvt fresh_permute_left)

   191   apply (simp add: fresh_Pair_elim Abs1_eq_iff lam.fresh)

   192   apply (case_tac "xaa = x")

   193   apply (simp_all add: fresh_Pair)[2]

   194   apply blast

   195   apply (rotate_tac -2)

   196   apply (drule_tac x="s1" in meta_spec)

   197   apply (rotate_tac -1)

   198   apply (drule_tac x="s2" in meta_spec)

   199   apply (rotate_tac -1)

   200   apply (drule_tac x="(atom x \<rightleftharpoons> atom xaa) \<bullet> t1" in meta_spec)

   201   apply (rotate_tac -1)

   202   apply (drule_tac x="(atom x \<rightleftharpoons> atom xaa) \<bullet> t2" in meta_spec)

   203   apply (rotate_tac -1)

   204   apply (simp add: One_preserves_fresh fresh_permute_left One.eqvt)

   205   by (metis Nominal2_Base.swap_commute One_preserves_fresh flip_def subst_rename)

   206 

   207 lemma One_Redex:

   208   assumes a: "App (Lam [x].t) s \<longrightarrow>1 r" "atom x \<sharp> (s,r)"

   209   shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>1 t' \<and> s \<longrightarrow>1 s') \<or>

   210          (\<exists>t' s'. r = t'[x ::= s'] \<and> t \<longrightarrow>1 t' \<and> s \<longrightarrow>1 s')"

   211   using a

   212   by (cases rule: One_strong_cases)

   213      (auto dest!: One_Lam simp add: fresh_Pair lam.fresh Abs1_eq_iff)

   214 

   215 inductive

   216   One_star :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>1* _" [80,80] 80)

   217 where

   218   os1[intro, simp]: "t \<longrightarrow>1* t"

   219 | os2[intro]: "t \<longrightarrow>1* r \<Longrightarrow> r \<longrightarrow>1 s \<Longrightarrow> t \<longrightarrow>1* s"

   220 

   221 lemma os3[intro, trans]:

   222   assumes a1: "M1 \<longrightarrow>1* M2"

   223   and     a2: "M2 \<longrightarrow>1* M3"

   224   shows "M1 \<longrightarrow>1* M3"

   225   using a2 a1

   226   by induct auto

   227 

   228 section {* Complete Development Reduction *}

   229 

   230 inductive

   231   Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>d _" [80,80] 80)

   232 where

   233   d1[intro]: "Var x \<longrightarrow>d Var x"

   234 | d2[intro]: "t \<longrightarrow>d s \<Longrightarrow> Lam [x].t \<longrightarrow>d Lam[x].s"

   235 | d3[intro]: "\<lbrakk>\<not>(\<exists>y t'. t1 = Lam [y].t'); t1 \<longrightarrow>d t2; s1 \<longrightarrow>d s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>d App t2 s2"

   236 | d4[intro]: "\<lbrakk>atom x \<sharp> (s1,s2); t1 \<longrightarrow>d t2; s1 \<longrightarrow>d s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>d t2[x::=s2]"

   237 

   238 equivariance Dev

   239 nominal_inductive Dev

   240   avoids d2: "x"

   241       |  d4: "x"

   242   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

   243 

   244 lemma better_d4_intro:

   245   assumes a: "t1 \<longrightarrow>d t2" "s1 \<longrightarrow>d s2"

   246   shows "App (Lam [x].t1) s1 \<longrightarrow>d t2[x::=s2]"

   247 proof -

   248   obtain y::"name" where fs: "atom y\<sharp>(x,t1,s1,t2,s2)" by (rule obtain_fresh)

   249   have "App (Lam [x].t1) s1 = App (Lam [y].((y \<leftrightarrow> x)\<bullet>t1)) s1" using fs

   250     by (auto simp add: Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)

   251   also have "\<dots> \<longrightarrow>d  ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: Dev.eqvt)

   252   also have "\<dots> = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])

   253   finally show "App (Lam [x].t1) s1 \<longrightarrow>d t2[x::=s2]" by simp

   254 qed

   255 

   256 lemma Dev_preserves_fresh:

   257   fixes x::"name"

   258   assumes a: "M\<longrightarrow>d N"

   259   shows "atom x\<sharp>M \<Longrightarrow> atom x\<sharp>N"

   260   using a

   261   by (induct, auto simp add: lam.fresh)

   262      (metis fresh_fact)+

   263 

   264 lemma Dev_Lam:

   265   assumes a: "Lam [x].M \<longrightarrow>d N"

   266   shows "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>d N'"

   267 proof -

   268   from a have "atom x \<sharp> Lam [x].M" by (simp add: lam.fresh)

   269   with a have "atom x \<sharp> N" by (simp add: Dev_preserves_fresh)

   270   with a show "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>d N'"

   271     apply (cases rule: Dev.cases)

   272     apply (auto simp add: Abs1_eq_iff lam.fresh)

   273     apply (rule_tac x="(atom xa \<rightleftharpoons> atom x) \<bullet> s" in exI)

   274     apply (auto simp add: fresh_permute_left lam.fresh)

   275     by (metis swap_commute Dev.eqvt)

   276 qed

   277 

   278 lemma Development_existence:

   279   shows "\<exists>M'. M \<longrightarrow>d M'"

   280 by (nominal_induct M rule: lam.strong_induct)

   281    (auto dest!: Dev_Lam intro: better_d4_intro)

   282 

   283 lemma Triangle:

   284   assumes a: "t \<longrightarrow>d t1" "t \<longrightarrow>1 t2"

   285   shows "t2 \<longrightarrow>1 t1"

   286 using a

   287 proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)

   288   case (d4 x s1 s2 t1 t1' t2)

   289   have  fc: "atom x\<sharp>t2" "atom x\<sharp>s1" by fact+

   290   have "App (Lam [x].t1) s1 \<longrightarrow>1 t2" by fact

   291   then obtain t' s' where reds:

   292              "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>1 t' \<and> s1 \<longrightarrow>1 s') \<or>

   293               (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>1 t' \<and> s1 \<longrightarrow>1 s')"

   294   using fc by (auto dest!: One_Redex)

   295   have ih1: "t1 \<longrightarrow>1 t' \<Longrightarrow>  t' \<longrightarrow>1 t1'" by fact

   296   have ih2: "s1 \<longrightarrow>1 s' \<Longrightarrow>  s' \<longrightarrow>1 s2" by fact

   297   { assume "t1 \<longrightarrow>1 t'" "s1 \<longrightarrow>1 s'"

   298     then have "App (Lam [x].t') s' \<longrightarrow>1 t1'[x::=s2]"

   299       using ih1 ih2 by (auto intro: better_o4_intro)

   300   }

   301   moreover

   302   { assume "t1 \<longrightarrow>1 t'" "s1 \<longrightarrow>1 s'"

   303     then have "t'[x::=s'] \<longrightarrow>1 t1'[x::=s2]"

   304       using ih1 ih2 by (auto intro: One_subst)

   305   }

   306   ultimately show "t2 \<longrightarrow>1 t1'[x::=s2]" using reds by auto

   307 qed (auto dest!: One_Lam One_Var One_App)

   308 

   309 lemma Diamond_for_One:

   310   assumes a: "t \<longrightarrow>1 t1" "t \<longrightarrow>1 t2"

   311   shows "\<exists>t3. t2 \<longrightarrow>1 t3 \<and> t1 \<longrightarrow>1 t3"

   312 proof -

   313   obtain tc where "t \<longrightarrow>d tc" using Development_existence by blast

   314   with a have "t2 \<longrightarrow>1 tc" and "t1 \<longrightarrow>1 tc" by (simp_all add: Triangle)

   315   then show "\<exists>t3. t2 \<longrightarrow>1 t3 \<and> t1 \<longrightarrow>1 t3" by blast

   316 qed

   317 

   318 lemma Rectangle_for_One:

   319   assumes a:  "t \<longrightarrow>1* t1" "t \<longrightarrow>1 t2"

   320   shows "\<exists>t3. t1 \<longrightarrow>1 t3 \<and> t2 \<longrightarrow>1* t3"

   321 using a Diamond_for_One by (induct arbitrary: t2) (blast)+

   322 

   323 lemma CR_for_One_star:

   324   assumes a: "t \<longrightarrow>1* t1" "t \<longrightarrow>1* t2"

   325     shows "\<exists>t3. t2 \<longrightarrow>1* t3 \<and> t1 \<longrightarrow>1* t3"

   326 using a Rectangle_for_One by (induct arbitrary: t2) (blast)+

   327 

   328 section {* Establishing the Equivalence of Beta-star and One-star *}

   329 

   330 lemma Beta_Lam_cong:

   331   assumes a: "t1 \<longrightarrow>b* t2"

   332   shows "Lam [x].t1 \<longrightarrow>b* Lam [x].t2"

   333 using a by (induct) (blast)+

   334 

   335 lemma Beta_App_cong_aux:

   336   assumes a: "t1 \<longrightarrow>b* t2"

   337   shows "App t1 s\<longrightarrow>b* App t2 s"

   338     and "App s t1 \<longrightarrow>b* App s t2"

   339 using a by (induct) (blast)+

   340 

   341 lemma Beta_App_cong:

   342   assumes a: "t1 \<longrightarrow>b* t2" "s1 \<longrightarrow>b* s2"

   343   shows "App t1 s1 \<longrightarrow>b* App t2 s2"

   344 using a by (blast intro: Beta_App_cong_aux)

   345 

   346 lemmas Beta_congs = Beta_Lam_cong Beta_App_cong

   347 

   348 lemma One_implies_Beta_star:

   349   assumes a: "t \<longrightarrow>1 s"

   350   shows "t \<longrightarrow>b* s"

   351 using a by (induct, auto intro!: Beta_congs)

   352   (metis (hide_lams, no_types) Beta_App_cong_aux(1) Beta_App_cong_aux(2) Beta_Lam_cong b4 bs2 bs3 fresh_PairD(2))

   353 

   354 lemma One_congs:

   355   assumes a: "t1 \<longrightarrow>1* t2"

   356   shows "Lam [x].t1 \<longrightarrow>1* Lam [x].t2"

   357   and   "App t1 s \<longrightarrow>1* App t2 s"

   358   and   "App s t1 \<longrightarrow>1* App s t2"

   359 using a by (induct) (auto intro: One_refl)

   360 

   361 lemma Beta_implies_One_star:

   362   assumes a: "t1 \<longrightarrow>b t2"

   363   shows "t1 \<longrightarrow>1* t2"

   364 using a by (induct) (auto intro: One_refl One_congs better_o4_intro)

   365 

   366 lemma Beta_star_equals_One_star:

   367   shows "t1 \<longrightarrow>1* t2 = t1 \<longrightarrow>b* t2"

   368 proof

   369   assume "t1 \<longrightarrow>1* t2"

   370   then show "t1 \<longrightarrow>b* t2" by (induct) (auto intro: One_implies_Beta_star)

   371 next

   372   assume "t1 \<longrightarrow>b* t2"

   373   then show "t1 \<longrightarrow>1* t2" by (induct) (auto intro: Beta_implies_One_star)

   374 qed

   375 

   376 section {* The Church-Rosser Theorem *}

   377 

   378 theorem CR_for_Beta_star:

   379   assumes a: "t \<longrightarrow>b* t1" "t\<longrightarrow>b* t2"

   380   shows "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3"

   381 proof -

   382   from a have "t \<longrightarrow>1* t1" and "t\<longrightarrow>1* t2" by (simp_all add: Beta_star_equals_One_star)

   383   then have "\<exists>t3. t1 \<longrightarrow>1* t3 \<and> t2 \<longrightarrow>1* t3" by (simp add: CR_for_One_star)

   384   then show "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3" by (simp add: Beta_star_equals_One_star)

   385 qed

   386 

   387 end