Step
*
of Lemma
ml-filter-sq
β[A:Type]. β[P:A βΆ πΉ]. β[l:A List]. (ml-filter(P;l) ~ filter(P;l)) supposing valueall-type(A) β§ A
BY
{ (InductionOnList
THEN All (RepUR ``ml-filter spreadcons ml_apply``)
THEN (Assert valueall-type(A βΆ πΉ) BY
Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN RW (SweepUpC UnrollRecursionC) 0
THEN Reduce 0
THEN (Trivialβ
ORELSE ((CallByValueReduceOn βPβ 0β
THENA Auto) THEN Reduce 0))
THEN (CallByValueReduceOn βuβ 0β
THENA Auto)
THEN (All (CallByValueReduceOn βvβ β
)β
THENA Auto)
THEN (All (CallByValueReduceOn βPβ β
)β
THENA Auto)
THEN HypSubst' (-2) 0
THEN Auto) }
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[P:A {}\mrightarrow{} \mBbbB{}]. \mforall{}[l:A List]. (ml-filter(P;l) \msim{} filter(P;l)) supposing valueall-type(A) \mwedge{} A
By
Latex:
(InductionOnList
THEN All (RepUR ``ml-filter spreadcons ml\_apply``)
THEN (Assert valueall-type(A {}\mrightarrow{} \mBbbB{}) BY
Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN RW (SweepUpC UnrollRecursionC) 0
THEN Reduce 0
THEN (Trivial\mcdot{} ORELSE ((CallByValueReduceOn \mkleeneopen{}P\mkleeneclose{} 0\mcdot{} THENA Auto) THEN Reduce 0))
THEN (CallByValueReduceOn \mkleeneopen{}u\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (All (CallByValueReduceOn \mkleeneopen{}v\mkleeneclose{} \mcdot{})\mcdot{} THENA Auto)
THEN (All (CallByValueReduceOn \mkleeneopen{}P\mkleeneclose{} \mcdot{})\mcdot{} THENA Auto)
THEN HypSubst' (-2) 0
THEN Auto)
Home
Index