---

Step * of Lemma f-lattice_wf

∀[X:Type]. (f-lattice(X) ∈ BoundedDistributiveLattice)
BY
{ ((Intro
    THEN (Assert ((X + X) List List) ⊆r Point(free-dl(X + X)) BY
                ((Subst' Point(free-dl(X + X)) ~ free-dl-type(X + X) 0 THENA Computation) THEN Auto))
    )
   THEN (InstLemma `flattice-equiv-equiv` [⌜X⌝]⋅ THENA Auto)
   THEN ProveWfLemma
   THEN All (Unfold `flattice-equiv`)
   THEN SqExRepD
   THEN D 0) }

1
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)
⊢ ∃as,bs:(X + X) List List
   ((a ∧ b = as ∈ Point(free-dl(X + X)))
   ∧ (c ∧ d = bs ∈ Point(free-dl(X + X)))
   ∧ flattice-order(X;as;bs)
   ∧ flattice-order(X;bs;as))

2
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)
⊢ ∃as,bs:(X + X) List List
   ((a ∨ b = as ∈ Point(free-dl(X + X)))
   ∧ (c ∨ d = bs ∈ Point(free-dl(X + X)))
   ∧ flattice-order(X;as;bs)
   ∧ flattice-order(X;bs;as))

---

Latex:

---

Latex:
\mforall{}[X:Type].  (f-lattice(X)  \mmember{}  BoundedDistributiveLattice)


By

---

Latex:
((Intro
    THEN  (Assert  ((X  +  X)  List  List)  \msubseteq{}r  Point(free-dl(X  +  X))  BY
                            ((Subst'  Point(free-dl(X  +  X))  \msim{}  free-dl-type(X  +  X)  0  THENA  Computation)  THEN  Auto))
    )
  THEN  (InstLemma  `flattice-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ProveWfLemma
  THEN  All  (Unfold  `flattice-equiv`)
  THEN  SqExRepD
  THEN  D  0)

---

Home Index