---

Step * of Lemma flattice-order_transitivity

∀[X:Type]. ∀as,bs,cs:(X + X) List List.  (flattice-order(X;as;bs) ⇒ flattice-order(X;bs;cs) ⇒ flattice-order(X;as;cs))
BY
{ (Auto
   THEN All (\h. (Unfold `flattice-order` h THEN (RWO "l_all_iff" h THENA Auto) THEN (RWO "l_exists_iff" h THENA Auto)))
   ⋅
   THEN RepeatFor 2 (ParallelLast)
   THEN D -1
   THEN Auto
   THEN ExRepD
   THEN (FHyp 5 [-2] THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

1
1. [X] : Type
2. as : (X + X) List List
3. bs : (X + X) List List
4. cs : (X + X) List List
5. ∀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))))
6. ∀b:(X + X) List
     ((b ∈ cs) ⇒ ((∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. ((a ∈ bs) ∧ a ⊆ b))))
7. b : (X + X) List
8. (b ∈ cs)
9. a : (X + X) List
10. (a ∈ bs)
11. a ⊆ b
12. x : X + X
13. (x ∈ a)
14. (∃y∈a. y = flip-union(x) ∈ (X + X))
⊢ (x ∈ b)

2
1. [X] : Type
2. as : (X + X) List List
3. bs : (X + X) List List
4. cs : (X + X) List List
5. ∀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))))
6. ∀b:(X + X) List
     ((b ∈ cs) ⇒ ((∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. ((a ∈ bs) ∧ a ⊆ b))))
7. b : (X + X) List
8. (b ∈ cs)
9. a : (X + X) List
10. (a ∈ bs)
11. a ⊆ b
12. x : X + X
13. (x ∈ a)
14. (∃y∈a. y = flip-union(x) ∈ (X + X))
15. (x ∈ b)
⊢ (∃y∈b. y = flip-union(x) ∈ (X + X))

3
1. [X] : Type
2. as : (X + X) List List
3. bs : (X + X) List List
4. cs : (X + X) List List
5. ∀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))))
6. ∀b:(X + X) List
     ((b ∈ cs) ⇒ ((∃x:X + X. ((x ∈ b) ∧ (∃y∈b. y = flip-union(x) ∈ (X + X)))) ∨ (∃a:(X + X) List. ((a ∈ bs) ∧ a ⊆ b))))
7. b : (X + X) List
8. (b ∈ cs)
9. a : (X + X) List
10. (a ∈ bs)
11. a ⊆ b
12. a1 : (X + X) List
13. (a1 ∈ as)
14. a1 ⊆ a
15. (a1 ∈ as)
⊢ a1 ⊆ b

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}as,bs,cs:(X  +  X)  List  List.
        (flattice-order(X;as;bs)  {}\mRightarrow{}  flattice-order(X;bs;cs)  {}\mRightarrow{}  flattice-order(X;as;cs))


By

---

Latex:
(Auto
  THEN  All  (\mbackslash{}h.  (Unfold  `flattice-order`  h
                                THEN  (RWO  "l\_all\_iff"  h  THENA  Auto)
                                THEN  (RWO  "l\_exists\_iff"  h  THENA  Auto)))\mcdot{}
  THEN  RepeatFor  2  (ParallelLast)
  THEN  D  -1
  THEN  Auto
  THEN  ExRepD
  THEN  (FHyp  5  [-2]  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index