---

Step * 3 of Lemma flattice-equiv-equiv


1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. Sym(Point(free-dl(X + X));x,y.flattice-equiv(X;x;y))
4. a : Point(free-dl(X + X))
5. b : Point(free-dl(X + X))
6. c : Point(free-dl(X + X))
7. flattice-equiv(X;a;b)
8. flattice-equiv(X;b;c)
⊢ flattice-equiv(X;a;c)
BY
{ (ParallelOp -2
   THEN Unfold `flattice-equiv` -1
   THEN SqExRepD
   THEN (Assert b1 = as ∈ Point(free-dl(X + X)) BY
               Eq)
   THEN (Subst' Point(free-dl(X + X)) ~ free-dl-type(X + X) -1 THENA Computation)
   THEN (EqTypeHD  (-1) THENA Auto)
   THEN D -1) }

1
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. Sym(Point(free-dl(X + X));x,y.flattice-equiv(X;x;y))
4. a : Point(free-dl(X + X))
5. b : Point(free-dl(X + X))
6. c : Point(free-dl(X + X))
7. a1 : (X + X) List List
8. b1 : (X + X) List List
9. a = a1 ∈ Point(free-dl(X + X))
10. b = b1 ∈ Point(free-dl(X + X))
11. flattice-order(X;a1;b1)
12. flattice-order(X;b1;a1)
13. as : (X + X) List List
14. bs : (X + X) List List
15. b = as ∈ Point(free-dl(X + X))
16. c = bs ∈ Point(free-dl(X + X))
17. flattice-order(X;as;bs)
18. flattice-order(X;bs;as)
19. b1 = as ∈ pertype(λas,bs. ((as ∈ (X + X) List List) ∧ (bs ∈ (X + X) List List) ∧ dlattice-eq(X + X;as;bs)))
20. b1 ∈ (X + X) List List
21. as ∈ (X + X) List List
22. b1 ⇒ as
23. as ⇒ b1
⊢ ↓∃as,bs:(X + X) List List
    ((a = as ∈ Point(free-dl(X + X)))
    ∧ (c = bs ∈ Point(free-dl(X + X)))
    ∧ flattice-order(X;as;bs)
    ∧ flattice-order(X;bs;as))

---

Latex:

---

Latex:

1.  X  :  Type
2.  ((X  +  X)  List  List)  \msubseteq{}r  Point(free-dl(X  +  X))
3.  Sym(Point(free-dl(X  +  X));x,y.flattice-equiv(X;x;y))
4.  a  :  Point(free-dl(X  +  X))
5.  b  :  Point(free-dl(X  +  X))
6.  c  :  Point(free-dl(X  +  X))
7.  flattice-equiv(X;a;b)
8.  flattice-equiv(X;b;c)
\mvdash{}  flattice-equiv(X;a;c)


By

---

Latex:
(ParallelOp  -2
  THEN  Unfold  `flattice-equiv`  -1
  THEN  SqExRepD
  THEN  (Assert  b1  =  as  BY
                          Eq)
  THEN  (Subst'  Point(free-dl(X  +  X))  \msim{}  free-dl-type(X  +  X)  -1  THENA  Computation)
  THEN  (EqTypeHD    (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index