---

Step * 2 2 of Lemma f-lattice_wf


1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
                                        ((x = as ∈ Point(free-dl(X + X)))
                                        ∧ (y = bs ∈ Point(free-dl(X + X)))
                                        ∧ flattice-order(X;as;bs)
                                        ∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
20. a ∨ b = (a1 @ as) ∈ Point(free-dl(X + X))
⊢ c ∨ d = (b1 @ bs) ∈ Point(free-dl(X + X))
BY
{ ((Subst' b1 @ bs ~ b1 ∨ bs 0 THENA Computation) THEN EqCDA THEN Eq) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  ((X  +  X)  List  List)  \msubseteq{}r  Point(free-dl(X  +  X))
3.  EquivRel(Point(free-dl(X  +  X));x,y.\mdownarrow{}\mexists{}as,bs:(X  +  X)  List  List
                                                                                ((x  =  as)
                                                                                \mwedge{}  (y  =  bs)
                                                                                \mwedge{}  flattice-order(X;as;bs)
                                                                                \mwedge{}  flattice-order(X;bs;as)))
4.  a  :  Point(free-dl(X  +  X))
5.  c  :  Point(free-dl(X  +  X))
6.  b  :  Point(free-dl(X  +  X))
7.  d  :  Point(free-dl(X  +  X))
8.  a1  :  (X  +  X)  List  List
9.  b1  :  (X  +  X)  List  List
10.  a  =  a1
11.  c  =  b1
12.  flattice-order(X;a1;b1)
13.  flattice-order(X;b1;a1)
14.  as  :  (X  +  X)  List  List
15.  bs  :  (X  +  X)  List  List
16.  b  =  as
17.  d  =  bs
18.  flattice-order(X;as;bs)
19.  flattice-order(X;bs;as)
20.  a  \mvee{}  b  =  (a1  @  as)
\mvdash{}  c  \mvee{}  d  =  (b1  @  bs)


By

---

Latex:
((Subst'  b1  @  bs  \msim{}  b1  \mvee{}  bs  0  THENA  Computation)  THEN  EqCDA  THEN  Eq)

---

Home Index