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


1. Type
2. X@i
3. (X X) List@i
4. λx,y. word-rel(X;x;y)^* (map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) v) []
5. (X X) List@i
6. map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) L ∈ ((X X) List)
⊢ word-rel(X;(L [case of inl(a) => inr a  inr(a) => inl a]) [u v];L v)
BY
(Unfold `word-rel` THEN InstConcl [⌜case of inl(a) => inr a  inr(a) => inl a⌝;⌜u⌝;⌜L⌝;⌜v⌝]⋅ THEN Auto) }

1
1. Type
2. X@i
3. (X X) List@i
4. λx,y. word-rel(X;x;y)^* (map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) v) []
5. (X X) List@i
6. map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) L ∈ ((X X) List)
⊢ case of inl(a) => inr a  inr(a) => inl -u

2
1. Type
2. X@i
3. (X X) List@i
4. λx,y. word-rel(X;x;y)^* (map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) v) []
5. (X X) List@i
6. map(λx.case of inl(a) => inr a  inr(a) => inl a;rev(v)) L ∈ ((X X) List)
7. case of inl(a) => inr a  inr(a) => inl -u
⊢ ((L [case of inl(a) => inr a  inr(a) => inl a]) [u v])
(L [case of inl(a) => inr a  inr(a) => inl a; u] v)
∈ ((X X) List)


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{}  word-rel(X;(L  @  [case  u  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a])  @  [u  /  v];L  @  v)


By


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




Home Index