---

Step * of Lemma fset-closure-exists2

No Annotations
∀[T:Type]
  ∀eq:EqDecider(T). ∀r:T ⟶ ℕ. ∀fs:{f:T ⟶ T| ∀x:T. r (f x) < r x supposing ¬((f x) = x ∈ T)}  List. ∀s:fset(T).
    ∃c:fset(T). (c = fs closure of s)
BY
{ ((Auto THEN InstLemma `fset-closure-exists` [⌜T⌝;⌜eq⌝;⌜r⌝;⌜fs⌝;⌜s⌝] ⋅) THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. r : T ⟶ ℕ
4. fs : {f:T ⟶ T| ∀x:T. r (f x) < r x supposing ¬((f x) = x ∈ T)}  List
5. s : fset(T)
⊢ (∀f∈fs.∀x:T. ((¬((f x) = x ∈ T)) ⇒ r (f x) < r x))

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  InstLemma  `fset-closure-exists`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}fs\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]  \mcdot{})  THEN  Auto)

---

Home Index