Step
*
3
1
2
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
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
BY
{ (FLemma `transitive-reflexive-closure_transitivity` [11;-1] THEN Auto) }
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
12. z : (X + X) List
13. \mlambda{}x,y. word-rel(X;x;y)\^{}* w1 z
14. \mlambda{}x,y. word-rel(X;x;y)\^{}* w z
\mvdash{} \mlambda{}x,y. word-rel(X;x;y)\^{}* c z
By
Latex:
(FLemma `transitive-reflexive-closure\_transitivity` [11;-1] THEN Auto)
Home
Index