Nuprl Lemma : aa_list_filtered_indices

T:Type.

l:T List.

g:

. aa_list_filter_indices(l) g

l

Proof

Definitions occuring in Statement : aa_list_filter_indices: aa_list_filter_indices(l), bool:

, nat:

, all:

x:A. B[x], apply: f a, function: x:A

B[x], universe: Type, sublist: L1

L2
Definitions : member: t

T, all:

x:A. B[x], aa_list_filter_indices: aa_list_filter_indices(l), bfalse: ff, btrue: tt, false: False, implies: P

Q, not:

A, le: A

B, so_apply: x[s], ifthenelse: if b then t else f fi , nat:

, or: P

Q, and: P

Q, assert:

b, null: null(as), tl: tl(l), uiff: uiff(P;Q), uimplies: b supposing a, unit: Unit, prop:

, uall:

[x:A]. B[x], bool:

, rev_implies: P

Q, iff: P

Q, it:

Lemmas : bool_wf, nat_wf, aa_sublist_reflexive, assert_of_bnot, eqff_to_assert, not_wf, bnot_wf, assert_wf, equal_wf, uiff_transitivity, eqtt_to_assert, le_wf, cons_sublist_cons, aa_list_filter_indices_wf, sublist_wf, sublist_tl, false_wf
\mforall{}T:Type. \mforall{}l:T List. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbB{}. aa\_list\_filter\_indices(l) g \msubseteq{} l Date html generated: 2013_03_20-AM-09_52_06 Last ObjectModification: 2012_11_27-AM-10_32_14 Home Index