---

Step * 1 of Lemma free-word-inv_wf

.....antecedent..... 
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. word-equiv(X;w1;w2)
9. free-word(X) = free-word(X) ∈ Type
10. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
⊢ word-equiv(X;free-word-inv(w1);free-word-inv(w2))
BY
{ ((ParallelOp -3 THEN ExRepD THEN (D 0 With ⌜free-word-inv(w)⌝  THENA (RepUR ``free-word-inv`` 0 THEN Auto)))
   THEN (InstLemma `transitive-reflexive-closure-map` 
         [⌜(X + X) List⌝;⌜λx,y. word-rel(X;x;y)⌝;⌜λw.free-word-inv(w)⌝]⋅
   THENM (Reduce -1 THEN D 0)
   )
   THEN Auto
   THEN All Reduce) }

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. 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))

---

Latex:

---

Latex:
.....antecedent..... 
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.  word-equiv(X;w1;w2)
9.  free-word(X)  =  free-word(X)
10.  \mforall{}w:(X  +  X)  List.  (free-word-inv(w)  \mmember{}  (X  +  X)  List)
\mvdash{}  word-equiv(X;free-word-inv(w1);free-word-inv(w2))


By

---

Latex:
((ParallelOp  -3
    THEN  ExRepD
    THEN  (D  0  With  \mkleeneopen{}free-word-inv(w)\mkleeneclose{}    THENA  (RepUR  ``free-word-inv``  0  THEN  Auto)))
  THEN  (InstLemma  `transitive-reflexive-closure-map` 
              [\mkleeneopen{}(X  +  X)  List\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  word-rel(X;x;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}w.free-word-inv(w)\mkleeneclose{}]\mcdot{}
  THENM  (Reduce  -1  THEN  D  0)
  )
  THEN  Auto
  THEN  All  Reduce)

---

Home Index