---

Step * 1 of Lemma dlattice-order-free-dl-meet


1. X : Type
2. a1 : X List List
3. b1 : X List List
4. as : X List List
5. b2 : X List List
6. (∀b∈b1.(∃a∈a1. a ⊆ b))
7. (∀b∈b2.(∃a∈as. a ⊆ b))
⊢ (∀b∈free-dl-meet(b1;b2).(∃a∈free-dl-meet(a1;as). a ⊆ b))
BY
{ ((All (RWO "l_all_iff") THENA Auto)
   THEN (All (RWO "l_exists_iff") THENA Auto)
   THEN RWO "member-free-dl-meet" 0
   THEN Auto) }

1
1. X : Type
2. a1 : X List List
3. b1 : X List List
4. as : X List List
5. b2 : X List List
6. ∀b:X List. ((b ∈ b1) ⇒ (∃a:X List. ((a ∈ a1) ∧ a ⊆ b)))
7. ∀b:X List. ((b ∈ b2) ⇒ (∃a:X List. ((a ∈ as) ∧ a ⊆ b)))
8. b : X List
9. ∃u,v:X List. ((u ∈ b1) ∧ (v ∈ b2) ∧ (b = (u @ v) ∈ (X List)))
⊢ ∃a:X List. ((∃u,v:X List. ((u ∈ a1) ∧ (v ∈ as) ∧ (a = (u @ v) ∈ (X List)))) ∧ a ⊆ b)

---

Latex:

---

Latex:

1.  X  :  Type
2.  a1  :  X  List  List
3.  b1  :  X  List  List
4.  as  :  X  List  List
5.  b2  :  X  List  List
6.  (\mforall{}b\mmember{}b1.(\mexists{}a\mmember{}a1.  a  \msubseteq{}  b))
7.  (\mforall{}b\mmember{}b2.(\mexists{}a\mmember{}as.  a  \msubseteq{}  b))
\mvdash{}  (\mforall{}b\mmember{}free-dl-meet(b1;b2).(\mexists{}a\mmember{}free-dl-meet(a1;as).  a  \msubseteq{}  b))


By

---

Latex:
((All  (RWO  "l\_all\_iff")  THENA  Auto)
  THEN  (All  (RWO  "l\_exists\_iff")  THENA  Auto)
  THEN  RWO  "member-free-dl-meet"  0
  THEN  Auto)

---

Home Index