---

Step * 1 1 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. ↑fset-antichain(union-deq(T;T;eq;eq);x)
6. a : fset(T + T)
7. a ∈ x
8. z : T
9. ∀x:T + T. (x ∈ a ⇒ (∀c:fset(T + T). (c ∈ face-lattice-constraints(x) ⇒ (¬c ⊆ a))))
10. inl z ∈ T + T
11. inr z  ∈ T + T
⊢ ¬(inl z ∈ a ∧ inr z  ∈ a)
BY
{ ((D 0 THENA Auto) THEN (InstHyp [⌜inl z⌝;⌜{inl z,inr z }⌝] (-4)⋅ THENA Auto)) }

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. ↑fset-antichain(union-deq(T;T;eq;eq);x)
6. a : fset(T + T)
7. a ∈ x
8. z : T
9. ∀x:T + T. (x ∈ a ⇒ (∀c:fset(T + T). (c ∈ face-lattice-constraints(x) ⇒ (¬c ⊆ a))))
10. inl z ∈ T + T
11. inr z  ∈ T + T
12. inl z ∈ a
13. inr z  ∈ a
⊢ {inl z,inr z } ∈ face-lattice-constraints(inl z)

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

---

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.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
6.  a  :  fset(T  +  T)
7.  a  \mmember{}  x
8.  z  :  T
9.  \mforall{}x:T  +  T.  (x  \mmember{}  a  {}\mRightarrow{}  (\mforall{}c:fset(T  +  T).  (c  \mmember{}  face-lattice-constraints(x)  {}\mRightarrow{}  (\mneg{}c  \msubseteq{}  a))))
10.  inl  z  \mmember{}  T  +  T
11.  inr  z    \mmember{}  T  +  T
\mvdash{}  \mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}inl  z\mkleeneclose{};\mkleeneopen{}\{inl  z,inr  z  \}\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto))

---

Home Index