Step
*
1
1
2
1
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) []
⊢ (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)
BY
{ ((BLemma `transitive-reflexive-closure-base-case` THEN Auto) THEN Reduce 0) }
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) []
⊢ word-rel(X;map(λx.case x of inl(a) => inr a | inr(a) => inl a;rev(v) @ [u]) @ [u / v];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{} (map(\mlambda{}x.case x of inl(a) => inr a | inr(a) => inl a;rev(v) @ [u]) @ [u / v])
\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)
By
Latex:
((BLemma `transitive-reflexive-closure-base-case` THEN Auto) THEN Reduce 0)
Home
Index