---

Step * of Lemma fset-closure-exists

∀[T:Type]
  ∀eq:EqDecider(T). ∀r:T ⟶ ℕ. ∀fs:(T ⟶ T) List.
    ∀s:fset(T). ∃c:fset(T). (c = fs closure of s) supposing (∀f∈fs.∀x:T. ((¬((f x) = x ∈ T)) ⇒ r (f x) < r x))
BY
{ (Auto THEN (Assert ∀x,y:T.  Dec(x = y ∈ T) BY (Auto THEN BLemma `decidable-equal-deq` THEN Auto))) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. r : T ⟶ ℕ
4. fs : (T ⟶ T) List
5. (∀f∈fs.∀x:T. ((¬((f x) = x ∈ T)) ⇒ r (f x) < r x))
6. s : fset(T)
7. ∀x,y:T.  Dec(x = y ∈ T)
⊢ ∃c:fset(T). (c = fs closure of s)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}r:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}fs:(T  {}\mrightarrow{}  T)  List.
        \mforall{}s:fset(T).  \mexists{}c:fset(T).  (c  =  fs  closure  of  s) 
        supposing  (\mforall{}f\mmember{}fs.\mforall{}x:T.  ((\mneg{}((f  x)  =  x))  {}\mRightarrow{}  r  (f  x)  <  r  x))


By

---

Latex:
(Auto  THEN  (Assert  \mforall{}x,y:T.    Dec(x  =  y)  BY  (Auto  THEN  BLemma  `decidable-equal-deq`  THEN  Auto)))

---

Home Index