---

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


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]))) []
BY
{ ((Using [`y',⌜ys @ map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(ys))⌝]
       (BLemma  `transitive-reflexive-closure_transitivity`)⋅
    THEN Auto
    )
   THEN (BLemma `transitive-reflexive-closure-base-case` THEN Auto)
   THEN Reduce 0
   THEN (RWW "reverse_append_sq map_append_sq" 0 THENA Auto)
   THEN (GenConcl ⌜map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(ys)) = L ∈ ((X + X) List)⌝⋅ THENA Auto)
   THEN Reduce 0) }

1
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))) []
5. L : (X + X) List@i
6. map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(ys)) = L ∈ ((X + X) List)
⊢ word-rel(X;(ys @ [y]) @ [case y of inl(a) => inr a  | inr(a) => inl a / L];ys @ L)

---

Latex:

---

Latex:

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


By

---

Latex:
((Using  [`y',\mkleeneopen{}ys  @  map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(ys))\mkleeneclose{}]
          (BLemma    `transitive-reflexive-closure\_transitivity`)\mcdot{}
    THEN  Auto
    )
  THEN  (BLemma  `transitive-reflexive-closure-base-case`  THEN  Auto)
  THEN  Reduce  0
  THEN  (RWW  "reverse\_append\_sq  map\_append\_sq"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(ys))  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Reduce  0)

---

Home Index