Step
*
1
1
of Lemma
free-word-inv_wf
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List. (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. λx,y. word-rel(X;x;y)^* w1 w
10. λx,y. word-rel(X;x;y)^* w2 w
11. free-word(X) = free-word(X) ∈ Type
12. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
13. x : (X + X) List@i
14. y : (X + X) List@i
15. word-rel(X;x;y)
⊢ word-rel(X;free-word-inv(x);free-word-inv(y))
BY
{ (RenameVar `u' (-3) THEN RenameVar `v' (-2) THEN ParallelLast THEN ExRepD) }
1
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List. (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. λx,y. word-rel(X;x;y)^* w1 w
10. λx,y. word-rel(X;x;y)^* w2 w
11. free-word(X) = free-word(X) ∈ Type
12. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
13. u : (X + X) List@i
14. v : (X + X) List@i
15. x : X + X@i
16. y : X + X@i
17. a : (X + X) List@i
18. b : (X + X) List@i
19. x = -y
20. u = (a @ [x; y] @ b) ∈ ((X + X) List)
21. v = (a @ b) ∈ ((X + X) List)
⊢ ∃x,y:X + X
∃a,b:(X + X) List
(x = -y ∧ (free-word-inv(u) = (a @ [x; y] @ b) ∈ ((X + X) List)) ∧ (free-word-inv(v) = (a @ b) ∈ ((X + X) List)))
Latex:
Latex:
1. X : Type
2. (X + X) List \mmember{} Type
3. \mforall{}w1,w2:(X + X) List. (word-equiv(X;w1;w2) \mmember{} Type)
4. \mforall{}w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. \mlambda{}x,y. word-rel(X;x;y)\^{}* w1 w
10. \mlambda{}x,y. word-rel(X;x;y)\^{}* w2 w
11. free-word(X) = free-word(X)
12. \mforall{}w:(X + X) List. (free-word-inv(w) \mmember{} (X + X) List)
13. x : (X + X) List@i
14. y : (X + X) List@i
15. word-rel(X;x;y)
\mvdash{} word-rel(X;free-word-inv(x);free-word-inv(y))
By
Latex:
(RenameVar `u' (-3) THEN RenameVar `v' (-2) THEN ParallelLast THEN ExRepD)
Home
Index