---

Step * 1 1 2 1 1 1 1 of Lemma free-word-inv-append1


1. X : Type
2. u : X + X@i
3. v : (X + X) List@i
4. λx,y. word-rel(X;x;y)^* (map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v)) @ v) []
5. L : (X + X) List@i
6. map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v)) = L ∈ ((X + X) List)
⊢ case u of inl(a) => inr a  | inr(a) => inl a = -u
BY
{ ((All  Thin THEN D -1) THEN Reduce 0 THEN ((D 0 With ⌜x⌝  THEN Auto) ORELSE (D 0 With ⌜y⌝  THEN Auto))) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  u  :  X  +  X@i
3.  v  :  (X  +  X)  List@i
4.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  (map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(v))  @  v)  []
5.  L  :  (X  +  X)  List@i
6.  map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(v))  =  L
\mvdash{}  case  u  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a  =  -u


By

---

Latex:
((All    Thin  THEN  D  -1)
  THEN  Reduce  0
  THEN  ((D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)  ORELSE  (D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto)))

---

Home Index