wanted: Beweisbaum für Mitgliedschaft in Sprache eines regulären Ausdrucks

Inferenzbaum bzgl. der Regeln

• \displaystyle(\cup)\frac{w\in X} {w\in X+Y},
• \displaystyle(\cup)\frac{w\in Y} {w\in X+Y},
• \displaystyle(\cdot)\frac{u\in X,v\in Y}{u\cdot v\in X\cdot Y},
• \displaystyle(*)\frac{}{\epsilon\in X^*}
• \displaystyle(*)\frac{u\in X, v\in X^*}{u\cdot v\in X^*}

abstrakte Syntax:

data Claim c = Member { word :: [c], exp :: RX c, because :: Reason c } 
data Reason c 
  = Eps 
  | Letter
  | Union_Left (Claim c)
  | Union_Right (Claim c)
  | Dot {left :: Claim c, right :: Claim c }
  | Star_Zero
  | Star_Positive {left :: Claim c, right :: Claim c }
  | TODO -- zur Notation partieller Beweise