Try to prove stuff about container transducerscontainers

1 files changed, 15 insertions, 1 deletions

diff --git a/edit-lens/src/Control/Edit/Container/Transducer.lhs b/edit-lens/src/Control/Edit/Container/Transducer.lhs
index 9db26db..492ec91 100644
--- a/edit-lens/src/Control/Edit/Container/Transducer.lhs
+++ b/edit-lens/src/Control/Edit/Container/Transducer.lhs
@@ -154,7 +154,21 @@ Beweisskizze:
  Betrachte nun $\text{Replace}(c)$ gefolgt von $\text{Replace}(\text{init})$ unter $\text{diffContTrans}$ auf $\text{init}$.
  Für das Ergebnis $e_o^{-1}$ muss gelten, dass $e_o^{-1} \circ e_o = \text{id}$.
  Wir haben also Inverse für beliebige Elemente des edit-monoiden auf dem Output; also eine Gruppe auf edits auf dem Output die kompatibel ist mit der bestehenden monoid struktur.
- 
+
+Beweis:
+  Nimm an edits auf dem output-container $N$ bilden einen Monoiden, jedoch keine Gruppe, d.h. es existiert $e_o$ sodass für alle $e_o^\prime$, edits auf dem output-container, gilt, dass $e_o \cdot e_o^prime \neq 1$.
+  Es sei $M$ der Container mit genau einer Shape und belegten Position und ${\text{init}, c}$ als Inhalt mit $\text{Replace}$ als Modul-Struktur.
+  Es sei $T$ der Container-Transducer mit zwei Zuständen $A$ und $B$ und folgender Transitions-Funktion:
+  \begin{align*}
+    (A, \init) & \mapsto (1_{\partial N}, A)
+    (A, c) & \mapsto ((\text{init}_N \cdot)^{-1}(e_o), B)
+    (B, \init) & \mapsto (1_{\partial N}, B)
+    (B, c) & \mapsto (1_{\partial N}, B)
+  \end{align*}
+  Wir bezeichnen mit $T(x)$ den output des transducers beim Lauf auf $x$.
+  
+  Betrachte nun die edit-linse $(\Rrightarrow, \Lleftarrow)$ für $T$ und insbesondere $e_o^{-1} = \pi_2(\Rrightarrow(\pi_1(\Rrightarrow(\ground, \text{Replace}(c))), \text{Replace}(\text{init})))$.
+  Da $T(\text{init}_M) = \text{init}_N$ und $T(c) = e_o$ muss nun gelten, dass $e_o^{-1} \cdot e_o = \init_N$, also $\partial N$ eine Gruppe.
 \begin{code}
 diffContTrans :: forall state input output.
                  ( Container input, Container output