---

Step * of Lemma mset_ind_a

∀s:DSet. ∀Q:MSet{s} ⟶ ℙ.
  ((∀w:MSet{s}. SqStable(Q[w]))
  ⇒ Q[0{s}]
  ⇒ (∀x:|s|. Q[mset_inj{s}(x)])
  ⇒ (∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys']))
  ⇒ {∀zs:MSet{s}. Q[zs]})
BY
{ ((Unfold `guard` 0 THEN RepD) THENA Auto) }

1
1. s : DSet
2. Q : MSet{s} ⟶ ℙ
3. ∀w:MSet{s}. SqStable(Q[w])
4. Q[0{s}]
5. ∀x:|s|. Q[mset_inj{s}(x)]
6. ∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys'])
7. zs : MSet{s}
⊢ Q[zs]

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}Q:MSet\{s\}  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}w:MSet\{s\}.  SqStable(Q[w]))
    {}\mRightarrow{}  Q[0\{s\}]
    {}\mRightarrow{}  (\mforall{}x:|s|.  Q[mset\_inj\{s\}(x)])
    {}\mRightarrow{}  (\mforall{}ys,ys':MSet\{s\}.    (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  +  ys']))
    {}\mRightarrow{}  \{\mforall{}zs:MSet\{s\}.  Q[zs]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  RepD)  THENA  Auto)

---

Home Index