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