---

Step * of Lemma flattice-order-append

∀X:Type. ∀a1,b1,as,bs:(X + X) List List.
  (flattice-order(X;a1;b1) ⇒ flattice-order(X;as;bs) ⇒ flattice-order(X;a1 @ as;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_append" 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. (b ∈ b1) ∨ (b ∈ bs)
⊢ (∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. (((a ∈ a1) ∨ (a ∈ as)) ∧ 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;a1  @  as;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\_append"  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index