---

Step * 1 1 2 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) []
⊢ λx,y. word-rel(X;x;y)^* (map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v) @ [u]) @ [u / v]) []
BY
{ (Using [`y',⌜map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v)) @ v⌝]
      (BLemma  `transitive-reflexive-closure_transitivity`)⋅
   THEN Auto
   ) }

1
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) []
⊢ (map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v) @ [u]) @ [u / v]) 
  λx,y. word-rel(X;x;y)^* 
  (map(λx.case x of inl(a) => inr a  | inr(a) => inl a;rev(v)) @ v)

---

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)  []
\mvdash{}  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  (map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(v)  @  [u])  @  [u  /  \000Cv]) 
    []


By

---

Latex:
(Using  [`y',\mkleeneopen{}map(\mlambda{}x.case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a;rev(v))  @  v\mkleeneclose{}]
        (BLemma    `transitive-reflexive-closure\_transitivity`)\mcdot{}
  THEN  Auto
  )

---

Home Index