---

Step * 1 1 of Lemma free-dlwc-inc_wf


1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : T
5. ↑fset-null({c ∈ Cs[x] | deq-f-subset(eq) c {x}})
6. ↑fset-antichain(eq;{{x}})
7. a : fset(T)
8. a = {x} ∈ fset(T)
9. x1 : T
10. x1 ∈ {x}
11. c : fset(T)
12. c ∈ Cs[x1]
⊢ ¬c ⊆ {x}
BY
{ OnMaybeHyp 5 (\h. ((RWO "assert-fset-null" h THENA Auto)
                     THEN (InstLemma `fset-filter-is-empty` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
                     THEN (RWO "-1" h THENA Auto)
                     THEN ParallelOp h
                     THEN With ⌜c⌝ (D 0)⋅
                     THEN Auto
                     THEN RWW "assert-deq-f-subset" 0
                     THEN Auto
                     THEN ∀j:hyp. ((RWO "member-fset-singleton" j THENA Auto)
                                   THEN RevHypSubst
                                   j 0⋅
                                   THEN Complete (Auto)) )) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  Cs  :  T  {}\mrightarrow{}  fset(fset(T))
4.  x  :  T
5.  \muparrow{}fset-null(\{c  \mmember{}  Cs[x]  |  deq-f-subset(eq)  c  \{x\}\})
6.  \muparrow{}fset-antichain(eq;\{\{x\}\})
7.  a  :  fset(T)
8.  a  =  \{x\}
9.  x1  :  T
10.  x1  \mmember{}  \{x\}
11.  c  :  fset(T)
12.  c  \mmember{}  Cs[x1]
\mvdash{}  \mneg{}c  \msubseteq{}  \{x\}


By

---

Latex:
OnMaybeHyp  5  (\mbackslash{}h.  ((RWO  "assert-fset-null"  h  THENA  Auto)
                                      THEN  (InstLemma  `fset-filter-is-empty`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                      THEN  (RWO  "-1"  h  THENA  Auto)
                                      THEN  ParallelOp  h
                                      THEN  With  \mkleeneopen{}c\mkleeneclose{}  (D  0)\mcdot{}
                                      THEN  Auto
                                      THEN  RWW  "assert-deq-f-subset"  0
                                      THEN  Auto
                                      THEN  \mforall{}j:hyp.  ((RWO  "member-fset-singleton"  j  THENA  Auto)
                                                                  THEN  RevHypSubst
                                                                  j  0\mcdot{}
                                                                  THEN  Complete  (Auto))  ))

---

Home Index