---

Step * 2 1 of Lemma face-lattice-basis


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-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. s : fset(T + T)
7. u : T + T
⊢ ↑fset-null({c ∈ face-lattice-constraints(u) | deq-f-subset(union-deq(T;T;eq;eq)) c {u}})
BY
{ (D -1
   THEN RepUR ``face-lattice-constraints`` 0
   THEN RepUR ``fset-filter fset-null fset-singleton`` 0
   THEN Fold `fset-singleton` 0
   THEN AutoSplit
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN MoveToConcl (-1)
   THEN RenameVar `z' (-1)
   THEN (Assert ¬((inl z) = (inr z ) ∈ (T + T)) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜(inl z) = a ∈ (T + T)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(inr z ) = b ∈ (T + T)⌝⋅ THENA Auto)
   THEN (RWO "eqtt_to_assert" 0 THENA Auto)
   THEN (RWO "assert-deq-f-subset" 0 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-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. s : fset(T + T)
7. z : T
8. a : T + T
9. (inl z) = a ∈ (T + T)
10. b : T + T
11. (inr z ) = b ∈ (T + T)
⊢ (¬(a = b ∈ (T + T))) ⇒ {a,b} ⊆ {a} ⇒ False

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-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. s : fset(T + T)
7. z : T
8. a : T + T
9. (inl z) = a ∈ (T + T)
10. b : T + T
11. (inr z ) = b ∈ (T + T)
⊢ (¬(a = b ∈ (T + T))) ⇒ {a,b} ⊆ {b} ⇒ 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.  fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6.  s  :  fset(T  +  T)
7.  u  :  T  +  T
\mvdash{}  \muparrow{}fset-null(\{c  \mmember{}  face-lattice-constraints(u)  |  deq-f-subset(union-deq(T;T;eq;eq))  c  \{u\}\})


By

---

Latex:
(D  -1
  THEN  RepUR  ``face-lattice-constraints``  0
  THEN  RepUR  ``fset-filter  fset-null  fset-singleton``  0
  THEN  Fold  `fset-singleton`  0
  THEN  AutoSplit
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  MoveToConcl  (-1)
  THEN  RenameVar  `z'  (-1)
  THEN  (Assert  \mneg{}((inl  z)  =  (inr  z  ))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(inl  z)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(inr  z  )  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "eqtt\_to\_assert"  0  THENA  Auto)
  THEN  (RWO  "assert-deq-f-subset"  0  THENA  Auto))

---

Home Index