---

Step * 2 1 of Lemma fl-point


1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. x1 : T + T
10. x1 ∈ a
11. c : fset(T + T)
12. c ∈ face-lattice-constraints(x1)
⊢ ¬c ⊆ a
BY
{ (D -4
   THEN RepUR ``face-lattice-constraints`` -1
   THEN (RWO "member-fset-singleton" (-1) THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RenameVar `z' (-4)
   THEN (Assert ¬(inl z ∈ a ∧ inr z  ∈ a) BY
               Auto)
   THEN ParallelLast
   THEN Auto
   THEN Try ((BackThruHyp' (-2) THEN EAuto 1))) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. z : T
10. inr z  ∈ a
11. c : fset(T + T)
12. c = {inl z,inr z } ∈ fset(T + T)
13. {inl z,inr z } ⊆ a
⊢ inl z ∈ a

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  fset(fset(T  +  T))
4.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
5.  \mforall{}a:fset(T  +  T).  (a  \mmember{}  x  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a))))
6.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
7.  a  :  fset(T  +  T)
8.  a  \mmember{}  x
9.  x1  :  T  +  T
10.  x1  \mmember{}  a
11.  c  :  fset(T  +  T)
12.  c  \mmember{}  face-lattice-constraints(x1)
\mvdash{}  \mneg{}c  \msubseteq{}  a


By

---

Latex:
(D  -4
  THEN  RepUR  ``face-lattice-constraints``  -1
  THEN  (RWO  "member-fset-singleton"  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RenameVar  `z'  (-4)
  THEN  (Assert  \mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)  BY
                          Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  Try  ((BackThruHyp'  (-2)  THEN  EAuto  1)))

---

Home Index