---

Step * of Lemma fset-induction

∀[T:Type]
  ∀eq:EqDecider(T)
    ∀[P:fset(T) ⟶ ℙ]
      ((∀s:fset(T). SqStable(P[s]))
      ⇒ P[{}]
      ⇒ (∀s:fset(T). ∀x:T.  (P[s] ⇒ P[fset-add(eq;x;s)] supposing ¬x ∈ s))
      ⇒ {∀s:fset(T). P[s]})
BY
{ TACTIC:(Unfold `guard` 0 THEN Auto THEN MoveToConcl (-1)) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. [P] : fset(T) ⟶ ℙ
4. ∀s:fset(T). SqStable(P[s])
5. P[{}]
6. ∀s:fset(T). ∀x:T.  (P[s] ⇒ P[fset-add(eq;x;s)] supposing ¬x ∈ s)
⊢ ∀s:fset(T). P[s]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T)
        \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}s:fset(T).  SqStable(P[s]))
            {}\mRightarrow{}  P[\{\}]
            {}\mRightarrow{}  (\mforall{}s:fset(T).  \mforall{}x:T.    (P[s]  {}\mRightarrow{}  P[fset-add(eq;x;s)]  supposing  \mneg{}x  \mmember{}  s))
            {}\mRightarrow{}  \{\mforall{}s:fset(T).  P[s]\})


By

---

Latex:
TACTIC:(Unfold  `guard`  0  THEN  Auto  THEN  MoveToConcl  (-1))

---

Home Index