---

Step * 1 1 2 1 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))) []
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)
BY
{ (Unfold `word-rel` 0 THEN InstConcl [⌜y⌝;⌜case y of inl(a) => inr a  | inr(a) => inl a⌝;⌜ys⌝;⌜L⌝]⋅ THEN Auto) }

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)
⊢ y = -case y of inl(a) => inr a  | inr(a) => inl a

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))) []
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)
7. y = -case y of inl(a) => inr a  | inr(a) => inl a
⊢ ((ys @ [y]) @ [case y of inl(a) => inr a  | inr(a) => inl a / L])
= (ys @ [y; case y of inl(a) => inr a  | inr(a) => inl a] @ L)
∈ ((X + X) List)

---

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


By

---

Latex:
(Unfold  `word-rel`  0
  THEN  InstConcl  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}case  y  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a\mkleeneclose{};\mkleeneopen{}ys\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index