---

Step * 1 1 1 1 of Lemma fset-minimals-ac-le


1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. n : ℤ
6. 0 < n
7. ∀x:fset(T)
     (||x|| < n - 1
     ⇒ x ∈ s
     ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))
8. x : fset(T)
9. ||x|| < n
10. x ∈ s
11. {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T))
⊢ False
BY
{ Assert ⌜x ∈ {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x}⌝⋅ }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. n : ℤ
6. 0 < n
7. ∀x:fset(T)
     (||x|| < n - 1
     ⇒ x ∈ s
     ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))
8. x : fset(T)
9. ||x|| < n
10. x ∈ s
11. {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T))
⊢ x ∈ {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x}

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. n : ℤ
6. 0 < n
7. ∀x:fset(T)
     (||x|| < n - 1
     ⇒ x ∈ s
     ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))
8. x : fset(T)
9. ||x|| < n
10. x ∈ s
11. {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T))
12. x ∈ {y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x}
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  s  :  fset(fset(T))
4.  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T))].
          uiff(fset-all(s;x.P[x]);\mforall{}[x:fset(T)].  \muparrow{}P[x]  supposing  x  \mmember{}  s)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}x:fset(T)
          (||x||  <  n  -  1
          {}\mRightarrow{}  x  \mmember{}  s
          {}\mRightarrow{}  (\mneg{}(\{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}
                =  \{\})))
8.  x  :  fset(T)
9.  ||x||  <  n
10.  x  \mmember{}  s
11.  \{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}  =  \{\}
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}x  \mmember{}  \{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}\mkleeneclose{}\mcdot{}

---

Home Index