---

Step * of Lemma flattice-order-meet

∀X:Type. ∀a1,b1,as,bs:(X + X) List List.
  (flattice-order(X;a1;b1) ⇒ flattice-order(X;as;bs) ⇒ flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs)))
BY
{ (Auto
   THEN All (Unfold  `flattice-order`)
   THEN (All (RWO "l_all_iff") THENA Auto)
   THEN (All (RWO "l_exists_iff") THENA Auto)
   THEN RWO "member-free-dl-meet" 0
   THEN Auto
   THEN ExRepD) }

1
1. X : Type
2. a1 : (X + X) List List
3. b1 : (X + X) List List
4. as : (X + X) List List
5. bs : (X + X) List List
6. ∀b:(X + X) List
     ((b ∈ b1) ⇒ ((∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. ((a ∈ a1) ∧ a ⊆ b))))
7. ∀b:(X + X) List
     ((b ∈ bs) ⇒ ((∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. ((a ∈ as) ∧ a ⊆ b))))
8. b : (X + X) List
9. u : (X + X) List
10. v : (X + X) List
11. (u ∈ b1)
12. (v ∈ bs)
13. b = (u @ v) ∈ ((X + X) List)
⊢ (∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X))))
∨ (∃a:(X + X) List. ((∃u,v:(X + X) List. ((u ∈ a1) ∧ (v ∈ as) ∧ (a = (u @ v) ∈ ((X + X) List)))) ∧ a ⊆ b))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}a1,b1,as,bs:(X  +  X)  List  List.
    (flattice-order(X;a1;b1)
    {}\mRightarrow{}  flattice-order(X;as;bs)
    {}\mRightarrow{}  flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs)))


By

---

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

---

Home Index