---

Step * of Lemma free-dl_wf

∀[X:Type]. (free-dl(X) ∈ BoundedDistributiveLattice)
BY
{ (Intro THEN (InstLemma `dlattice-eq-equiv` [⌜X⌝]⋅ THENA Auto) THEN ProveWfLemma) }

1
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
⊢ [] ∈ free-dl-type(X)

2
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
⊢ [[]] ∈ free-dl-type(X)

3
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. a : free-dl-type(X)
4. b : free-dl-type(X)
⊢ free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X)

4
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. a : free-dl-type(X)
5. b : free-dl-type(X)
⊢ free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X)

5
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. a : free-dl-type(X)
6. b : free-dl-type(X)
7. c : free-dl-type(X)
⊢ free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X)

6
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. a : free-dl-type(X)
7. b : free-dl-type(X)
8. c : free-dl-type(X)
⊢ free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X)

7
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. a : free-dl-type(X)
8. b : free-dl-type(X)
⊢ free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X)

8
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. a : free-dl-type(X)
9. b : free-dl-type(X)
⊢ free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X)

9
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. a : free-dl-type(X)
⊢ free-dl-meet(a;[[]]) = a ∈ free-dl-type(X)

10
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. a : free-dl-type(X)
⊢ free-dl-join(a;[]) = a ∈ free-dl-type(X)

11
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. ∀[a:free-dl-type(X)]. (free-dl-join(a;[]) = a ∈ free-dl-type(X))
11. a : free-dl-type(X)
12. b : free-dl-type(X)
13. c : free-dl-type(X)
⊢ free-dl-meet(a;free-dl-join(b;c)) = free-dl-join(free-dl-meet(a;b);free-dl-meet(a;c)) ∈ free-dl-type(X)

---

Latex:

---

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


By

---

Latex:
(Intro  THEN  (InstLemma  `dlattice-eq-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index