Nuprl Lemma : select-indices

{

[A:Type].

[f:A

].

[L:A List]. (select-indices(f;L)

List) }

{ Proof }

Definitions occuring in Statement : select-indices: select-indices(f;L), bool:

, nat:

, uall:

[x:A]. B[x], member: t

T, function: x:A

B[x], list: type List, universe: Type
Definitions : uall:

[x:A]. B[x], member: t

T, nat:

, select-indices: select-indices(f;L), le: A

B, not:

A, implies: P

Q, false: False, prop:

Lemmas : select-indices-aux_wf, le_wf, bool_wf

\mforall{}[A:Type]. \mforall{}[f:A {}\mrightarrow{} \mBbbB{}]. \mforall{}[L:A List]. (select-indices(f;L) \mmember{} \mBbbN{} List) Date html generated: 2011_08_17-PM-07_06_10 Last ObjectModification: 2011_06_18-PM-12_49_05 Home Index