Step
*
1
1
1
of Lemma
ball_respects_bsublist
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. ↑bsublist(s;us;vs)@i
5. Q : |s| ⟶ 𝔹@i
6. cs : |s| List
7. (cs @ us) ≡(|s|) vs
8. ↑(For{<𝔹,∧b>} x ∈ cs @ us. Q[x])
⊢ ↑(For{<𝔹,∧b>} x ∈ us. Q[x])
BY
{ (((RWH (LemmaC `mon_for_append`) 8 THENM AbReduce 8) THENM RW bool_to_propC 8) THEN Auto) }
Latex:
Latex:
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. \muparrow{}bsublist(s;us;vs)@i
5. Q : |s| {}\mrightarrow{} \mBbbB{}@i
6. cs : |s| List
7. (cs @ us) \mequiv{}(|s|) vs
8. \muparrow{}(For\{<\mBbbB{},\mwedge{}\msubb{}>\} x \mmember{} cs @ us. Q[x])
\mvdash{} \muparrow{}(For\{<\mBbbB{},\mwedge{}\msubb{}>\} x \mmember{} us. Q[x])
By
Latex:
(((RWH (LemmaC `mon\_for\_append`) 8 THENM AbReduce 8) THENM RW bool\_to\_propC 8) THEN Auto)
Home
Index