---

Step * of Lemma word-equiv-equiv

No Annotations
∀[X:Type]. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
BY
{ ((((InstLemma `word-rel-diamond` [] THEN Fold `rel-diamond-property` (-1) THEN Auto)
     THEN InstLemma `TC-equiv-is-equiv` [⌜(X + X) List⌝;⌜λx,y. word-rel(X;x;y)⌝]⋅
     )
    THENA (Reduce 0 THEN Auto THEN D 0 With ⌜λw.||w||⌝  THEN Reduce 0 THEN Auto THEN BLemma `word-rel-length` THEN Auto)
    )
   THEN (NthHypSq (-1) THEN Auto)
   THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))


By

---

Latex:
((((InstLemma  `word-rel-diamond`  []  THEN  Fold  `rel-diamond-property`  (-1)  THEN  Auto)
      THEN  InstLemma  `TC-equiv-is-equiv`  [\mkleeneopen{}(X  +  X)  List\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  word-rel(X;x;y)\mkleeneclose{}]\mcdot{}
      )
    THENA  (Reduce  0
                  THEN  Auto
                  THEN  D  0  With  \mkleeneopen{}\mlambda{}w.||w||\mkleeneclose{} 
                  THEN  Reduce  0
                  THEN  Auto
                  THEN  BLemma  `word-rel-length`
                  THEN  Auto)
    )
  THEN  (NthHypSq  (-1)  THEN  Auto)
  THEN  Computation)

---

Home Index