module Exercise_10 (module Join, module SafeMap) where

{- Library DO NOT CHANGE -}
import SafeMap (SafeMap, empty, update, lookup)
import Join (Field, doJoin, doJoinFormat, parseFormat)
{- End Library -}


{---------------------------------------------------------------------}
{- Aufgabe G10.1 -}

{-
\alpha ist wie in den Folien definiert.


Simulationseigenschaften:

R_empty: \alpha empty = {}
       : a      empty = {}


R_insert: \alpha (insert x xs) = {x} \union \alpha xs
        : a      (insert x xs) = {x}  union a      xs


R_isin: isin x xs = x \in \alpha xs
      : isin x xs = x  in a      xs


R_size: size xs = |\alpha xs|
      : size xs = |a      xs|



Hilfslemmata:

L_elem(xs): elem x xs = x in a xs
Proof by structural induction on xs

Base case: L_elem([])
To show:

Induction step: L_elem(ys) => Lemma(y : ys)
IH:
To show:


L_length(xs): length (nub xs) = |a xs| 
Proof by structural induction on xs

Base case: L_elem([])
To show:

Induction step: L_elem(ys) => Lemma(y : ys)
IH:
To show:

-}



{---------------------------------------------------------------------}
{- Aufgabe G10.2 -}

{- siehe SetPairList.hs -}



{---------------------------------------------------------------------}
{- Aufgabe G10.3 -}

{- siehe Queue.hs und SuperQueue.hs -}

{-
Definition von \alpha:

        \alpha (Queue front kcab) = undefined


Simulationseigenschaften: (5)



Beweise:
-}



{---------------------------------------------------------------------}
{- Aufgabe H10.1 -}

{- siehe SafeMap.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.2 -}

{- siehe Join.hs -}



{---------------------------------------------------------------------}
{- Aufgabe H10.3 -}

{- siehe Morsi.hs -}