Step
*
1
of Lemma
bsublist_transitivity
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. ws : |s| List@i
5. ↑bsublist(s;us;vs)@i
6. ↑bsublist(s;vs;ws)@i
⊢ ↑bsublist(s;us;ws)
BY
{ (OnMCls [6; 5; 0] (RWH (LemmaC `count_bsublist_a`)) THENA Auto) }
1
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. ws : |s| List@i
5. ∀c:|s|. ((c #∈ us) ≤ (c #∈ vs))
6. ∀c:|s|. ((c #∈ vs) ≤ (c #∈ ws))
⊢ ∀c:|s|. ((c #∈ us) ≤ (c #∈ ws))
Latex:
Latex:
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. ws : |s| List@i
5. \muparrow{}bsublist(s;us;vs)@i
6. \muparrow{}bsublist(s;vs;ws)@i
\mvdash{} \muparrow{}bsublist(s;us;ws)
By
Latex:
(OnMCls [6; 5; 0] (RWH (LemmaC `count\_bsublist\_a`)) THENA Auto)
Home
Index