---

Step * 3 1 of Lemma word-equiv-equiv


1. [X] : Type
2. Sym((X + X) List;w1,w2.∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w)))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. w1 : (X + X) List
7. λx,y. word-rel(X;x;y)^* a w1
8. λx,y. word-rel(X;x;y)^* b w1
9. w : (X + X) List
10. λx,y. word-rel(X;x;y)^* b w
11. λx,y. word-rel(X;x;y)^* c w
⊢ ∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* a w) ∧ (λx,y. word-rel(X;x;y)^* c w))
BY
{ ((InstLemma `word-rel-confluent` [⌜X⌝;⌜b⌝;⌜w1⌝;⌜w⌝]⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast)) }

1
1. [X] : Type
2. Sym((X + X) List;w1,w2.∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w)))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. w1 : (X + X) List
7. λx,y. word-rel(X;x;y)^* a w1
8. λx,y. word-rel(X;x;y)^* b w1
9. w : (X + X) List
10. λx,y. word-rel(X;x;y)^* b w
11. λx,y. word-rel(X;x;y)^* c w
12. z : (X + X) List
13. λx,y. word-rel(X;x;y)^* w z
14. λx,y. word-rel(X;x;y)^* w1 z
⊢ λx,y. word-rel(X;x;y)^* a z

2
1. [X] : Type
2. Sym((X + X) List;w1,w2.∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w)))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. w1 : (X + X) List
7. λx,y. word-rel(X;x;y)^* a w1
8. λx,y. word-rel(X;x;y)^* b w1
9. w : (X + X) List
10. λx,y. word-rel(X;x;y)^* b w
11. λx,y. word-rel(X;x;y)^* c w
12. z : (X + X) List
13. λx,y. word-rel(X;x;y)^* w1 z
14. λx,y. word-rel(X;x;y)^* w z
⊢ λx,y. word-rel(X;x;y)^* c z

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  Sym((X  +  X)  List;w1,w2.\mexists{}w:(X  +  X)  List
                                                      ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)))
3.  a  :  (X  +  X)  List
4.  b  :  (X  +  X)  List
5.  c  :  (X  +  X)  List
6.  w1  :  (X  +  X)  List
7.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  a  w1
8.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w1
9.  w  :  (X  +  X)  List
10.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w
11.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  c  w
\mvdash{}  \mexists{}w:(X  +  X)  List.  ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  a  w)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  c  w))


By

---

Latex:
((InstLemma  `word-rel-confluent`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}w1\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast))

---

Home Index