# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1633823807 -3600
# Node ID e51c9a67a68de9797628652353b137e878fba29f
# Parent  8bb064045b4e3a9f424445c4a83f46e910eb3f32
updated

diff -r 8bb064045b4e -r e51c9a67a68d thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/BitCoded2.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -173,6 +173,8 @@
 | "intern (STAR r) = ASTAR [S] (intern r)"
 
 
+
+
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
 | "retrieve (ACHAR bs c) (Char d) = bs"
diff -r 8bb064045b4e -r e51c9a67a68d thys/Exercises.thy
--- a/thys/Exercises.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Exercises.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -9,7 +9,7 @@
 where
   "zeroable (ZERO) \<longleftrightarrow> True"
 | "zeroable (ONE) \<longleftrightarrow> False"
-| "zeroable (CHAR c) \<longleftrightarrow> False"
+| "zeroable (CH c) \<longleftrightarrow> False"
 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2"
 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2"
 | "zeroable (STAR r) \<longleftrightarrow> False"
@@ -24,7 +24,7 @@
 where
   "atmostempty (ZERO) \<longleftrightarrow> True"
 | "atmostempty (ONE) \<longleftrightarrow> True"
-| "atmostempty (CHAR c) \<longleftrightarrow> False"
+| "atmostempty (CH c) \<longleftrightarrow> False"
 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"
 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> 
      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
@@ -37,7 +37,7 @@
 where
   "somechars (ZERO) \<longleftrightarrow> False"
 | "somechars (ONE) \<longleftrightarrow> False"
-| "somechars (CHAR c) \<longleftrightarrow> True"
+| "somechars (CH c) \<longleftrightarrow> True"
 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
 | "somechars (SEQ r1 r2) \<longleftrightarrow> 
       (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 
@@ -69,7 +69,7 @@
 where
   "leastsinglechar (ZERO) \<longleftrightarrow> False"
 | "leastsinglechar (ONE) \<longleftrightarrow> False"
-| "leastsinglechar (CHAR c) \<longleftrightarrow> True"
+| "leastsinglechar (CH c) \<longleftrightarrow> True"
 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2"
 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> 
       (if (zeroable r1 \<or> zeroable r2) then False
@@ -96,7 +96,7 @@
 where
   "infinitestrings (ZERO) = False"
 | "infinitestrings (ONE) = False"
-| "infinitestrings (CHAR c) = False"
+| "infinitestrings (CH c) = False"
 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"
 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 
       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"
diff -r 8bb064045b4e -r e51c9a67a68d thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Journal/Paper.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -5,7 +5,7 @@
    "../Simplifying" 
    "../Positions"
    "../Sulzmann"
-   "~~/src/HOL/Library/LaTeXsugar"
+   "HOL-Library.LaTeXsugar"
 begin
 
 lemma Suc_0_fold:
@@ -50,7 +50,7 @@
 
   ZERO ("\<^bold>0" 81) and 
   ONE ("\<^bold>1" 81) and 
-  CHAR ("_" [1000] 80) and
+  CH ("_" [1000] 80) and
   ALT ("_ + _" [77,77] 78) and
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [79] 78) and
@@ -333,7 +333,7 @@
   \<open>r :=\<close>
   @{const "ZERO"} $\mid$
   @{const "ONE"} $\mid$
-  @{term "CHAR c"} $\mid$
+  @{term "CH c"} $\mid$
   @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "STAR r"} 
@@ -1411,7 +1411,7 @@
 \begin{tabular}{lcl}
   @{term areg} & $::=$ & @{term "AZERO"}\\
                & $\mid$ & @{term "AONE bs"}\\
-               & $\mid$ & @{term "ACHAR bs c"}\\
+               & $\mid$ & @{term "ACH bs c"}\\
                & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\
                & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
                & $\mid$ & @{term "ASTAR bs r"}
@@ -1693,7 +1693,7 @@
   By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are
   straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to 
   @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)
-  where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption
+  where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption
   we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by 
   simplification of left- and right-hand side. In  case @{term "c \<noteq> d"} we have again
   @{term "\<Turnstile> v : ZERO"}, which cannot  hold. 
diff -r 8bb064045b4e -r e51c9a67a68d thys/Lexer.thy
--- a/thys/Lexer.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Lexer.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -15,7 +15,7 @@
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
-  "injval (CHAR d) c Void = Char d"
+  "injval (CH d) c Void = Char d"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
@@ -99,22 +99,22 @@
   then have "False" by cases
   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 next 
-  case (CHAR d)
+  case (CH d)
   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
-  then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+  then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
   proof (cases)
     case eq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ONE \<rightarrow> v" using eq by simp
     then have eqs: "s = [] \<and> v = Void" by cases simp
-    show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 
+    show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs 
     by (auto intro: Posix.intros)
   next
     case ineq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
     then have "False" by cases
-    then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
+    then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
   qed
 next
   case (ALT r1 r2)
diff -r 8bb064045b4e -r e51c9a67a68d thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Paper/Paper.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -15,13 +15,20 @@
 abbreviation 
  "ders_syn r s \<equiv> ders s r"
 
+(*
 notation (latex output)
-  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10)
+*)
+(*
+notation (latex output)
   Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
+*)
 
+(*
+notation (latex output)
   ZERO ("\<^bold>0" 78) and 
   ONE ("\<^bold>1" 78) and 
-  CHAR ("_" [1000] 80) and
+  CH ("_" [1000] 80) and
   ALT ("_ + _" [77,77] 78) and
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [1000] 78) and
@@ -55,9 +62,13 @@
   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
   slexer ("lexer\<^sup>+" 1000) and
+*)
 
+(*
+notation (latex output)
   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
+*)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -226,7 +237,7 @@
   @{text "r :="}
   @{const "ZERO"} $\mid$
   @{const "ONE"} $\mid$
-  @{term "CHAR c"} $\mid$
+  @{term "CH c"} $\mid$
   @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "STAR r"} 
@@ -405,7 +416,7 @@
   @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]
   @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm]
   @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  
-  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
+  %%@ { thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
   \end{tabular}
   \end{center}
 
@@ -1024,20 +1035,9 @@
 
 \begin{center}  
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
-
-@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
-@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
+??? &
+??? \smallskip\\
 
-@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
-@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
-
-@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
-@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
-
-@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
-@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
 \end{tabular}
 \end{center}
 
@@ -1062,7 +1062,9 @@
   What is interesting for our purposes is that the properties reflexivity,
   totality and transitivity for this GREEDY ordering can be proved
   relatively easily by induction.
+*}
 
+(*
   These properties of GREEDY, however, do not transfer to the POSIX
   ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
   To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
@@ -1071,7 +1073,9 @@
   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
   (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
   formulation, for example:
+*)
 
+text {*
   \begin{falsehood}
   Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
   If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
diff -r 8bb064045b4e -r e51c9a67a68d thys/Positions.thy
--- a/thys/Positions.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Positions.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -527,8 +527,8 @@
   then show "Void :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
-  case (Posix_CHAR c v)
-  have "v \<in> LV (CHAR c) [c]" by fact
+  case (Posix_CH c v)
+  have "v \<in> LV (CH c) [c]" by fact
   then have "v = Char c"
     by (simp add: LV_simps)
   then show "Char c :\<sqsubseteq>val v"
diff -r 8bb064045b4e -r e51c9a67a68d thys/ROOT
--- a/thys/ROOT	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/ROOT	Sun Oct 10 00:56:47 2021 +0100
@@ -1,39 +1,23 @@
-session "Lex" = HOL +
-  theories [document = false]
-        "Spec"
-	(*"SpecExt"*)
-        "Lexer"
-        (*"LexerExt"*)
-        "Simplifying"
-        "Sulzmann" 
-        "Positions"
-	(*"PositionsExt"*)
-        "Exercises"
 
-session Paper in "Paper" = Lex +
-  options [document = pdf, document_output = "..", document_variants="paper"]
-  theories 
-    "~~/src/HOL/Library/LaTeXsugar"
-    "Paper"
-  document_files
-    "root.bib"
-    "root.tex" 
 
 
-session Journal in "Journal" = HOL +
-  options [document = pdf, document_output = "..", document_variants="journal"]
+session Journal in Journal = "HOL" +
+  options [document_output = "..", document_variants="journal"]
+  sessions
+    "HOL-Library"
+  directories
+     ".." 
   theories [document = false]
-     "~~/src/HOL/Library/LaTeXsugar"
-     "~~/src/HOL/Library/Sublist"
+     "HOL-Library.LaTeXsugar"
+     "HOL-Library.Sublist"
      "../Spec"
+     "../Lexer"
      "../RegLangs"
-     "../Lexer"
      "../Simplifying"
      "../Sulzmann" 
-     "../Positions"
+     "../Positions"   
   theories [document = true] 
-    "Paper"
-    "PaperExt"
+     "Paper"
   document_files
-    "root.bib"
-    "root.tex" 
+     "root.bib"
+     "root.tex" 
\ No newline at end of file
diff -r 8bb064045b4e -r e51c9a67a68d thys/RegLangs.thy
--- a/thys/RegLangs.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/RegLangs.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -1,5 +1,5 @@
 theory RegLangs
-  imports Main "~~/src/HOL/Library/Sublist"
+  imports Main "HOL-Library.Sublist"
 begin
 
 section \<open>Sequential Composition of Languages\<close>
@@ -196,4 +196,41 @@
   shows "ders (s @ [c]) r = der c (ders s r)"
   by (simp add: ders_append)
 
+
+(*
+datatype ctxt = 
+    SeqC rexp bool
+  | AltCL rexp
+  | AltCR rexp 
+  | StarC rexp 
+
+function
+     down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+and  up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+where
+  "down c (SEQ r1 r2) ctxts =
+     (if (nullable r1) then down c r1 (SeqC r2 True # ctxts) 
+      else down c r1 (SeqC r2 False # ctxts))"
+| "down c (CH d) ctxts = 
+     (if c = d then up c ONE ctxts else up c ZERO ctxts)"
+| "down c ONE ctxts = up c ZERO ctxts"
+| "down c ZERO ctxts = up c ZERO ctxts"
+| "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)"
+| "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"
+| "up c r [] = (r, [])"
+| "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"
+| "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"
+| "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"
+| "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)"
+| "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"
+  apply(pat_completeness)
+  apply(auto)
+  done
+
+termination
+  sorry
+
+*)
+
+
 end
\ No newline at end of file
diff -r 8bb064045b4e -r e51c9a67a68d thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Sulzmann.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
@@ -88,7 +88,7 @@
 datatype arexp =
   AZERO
 | AONE "bit list"
-| ACHAR "bit list" char
+| ACH "bit list" char
 | ASEQ "bit list" arexp arexp
 | AALT "bit list" arexp arexp
 | ASTAR "bit list" arexp
@@ -96,7 +96,7 @@
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
-| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+| "fuse bs (ACH cs c) = ACH (bs @ cs) c"
 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
@@ -104,7 +104,7 @@
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACH [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
@@ -113,7 +113,7 @@
 
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
-| "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (ACH bs c) (Char d) = bs"
 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -126,7 +126,7 @@
 where
   "erase AZERO = ZERO"
 | "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACH _ c) = CH c"
 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)"
 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 | "erase (ASTAR _ r) = STAR (erase r)"
@@ -136,7 +136,7 @@
 where
   "bnullable (AZERO) = False"
 | "bnullable (AONE bs) = True"
-| "bnullable (ACHAR bs c) = False"
+| "bnullable (ACH bs c) = False"
 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)"
 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
 | "bnullable (ASTAR bs r) = True"
@@ -155,7 +155,7 @@
 where
   "bder c (AZERO) = AZERO"
 | "bder c (AONE bs) = AZERO"
-| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+| "bder c (ACH bs d) = (if c = d then AONE bs else AZERO)"
 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)"
 | "bder c (ASEQ bs r1 r2) = 
      (if bnullable r1