---

Step * 1 1 of Lemma free-word-inv-append2


1. X : Type
2. w1 : (X + X) List@i
⊢ λx,y. word-rel(X;x;y)^* (w1 @ map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(w1))) []
BY
{ (MoveToConcl (-1) THEN BLemma `last_induction` THEN Auto) }

1
1. X : Type
⊢ λx,y. word-rel(X;x;y)^* ([] @ map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev([]))) []

2
1. X : Type
2. ys : (X + X) List@i
3. y : X + X@i
4. λx,y. word-rel(X;x;y)^* (ys @ map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(ys))) []
⊢ λx,y. word-rel(X;x;y)^* ((ys @ [y]) @ map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(ys @ [y]))) []

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  BLemma  `last\_induction`  THEN  Auto)

---

Home Index