---

Step * 2 4 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))@i
5. c : Point(free-dl(X + X))@i
6. b : Point(free-dl(X + X))@i
7. d : Point(free-dl(X + X))@i
8. a1 : (X + X) List List@i
9. b1 : (X + X) List List@i
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@i
15. bs : (X + X) List List@i
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))
21. c ∨ d = (b1 @ bs) ∈ Point(free-dl(X + X))
22. flattice-order(X;a1 @ as;b1 @ bs)
⊢ flattice-order(X;b1 @ bs;a1 @ as)
BY
{ (FLemma `flattice-order-append` [13;19] THEN Auto) }

---

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))@i
5.  c  :  Point(free-dl(X  +  X))@i
6.  b  :  Point(free-dl(X  +  X))@i
7.  d  :  Point(free-dl(X  +  X))@i
8.  a1  :  (X  +  X)  List  List@i
9.  b1  :  (X  +  X)  List  List@i
10.  a  =  a1
11.  c  =  b1
12.  flattice-order(X;a1;b1)
13.  flattice-order(X;b1;a1)
14.  as  :  (X  +  X)  List  List@i
15.  bs  :  (X  +  X)  List  List@i
16.  b  =  as
17.  d  =  bs
18.  flattice-order(X;as;bs)
19.  flattice-order(X;bs;as)
20.  a  \mvee{}  b  =  (a1  @  as)
21.  c  \mvee{}  d  =  (b1  @  bs)
22.  flattice-order(X;a1  @  as;b1  @  bs)
\mvdash{}  flattice-order(X;b1  @  bs;a1  @  as)


By

---

Latex:
(FLemma  `flattice-order-append`  [13;19]  THEN  Auto)

---

Home Index