Nuprl Lemma : shifted-sequence

[T:Type].

f:

T.

a:T List. (shifted-sequence(f;a)

T)

Proof

Definitions occuring in Statement : shifted-sequence: shifted-sequence(f;a), nat:

, uall:

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

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

T, function: x:A

B[x], universe: Type
Definitions : uall:

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

x:A. B[x], nat:

, member: t

T, shifted-sequence: shifted-sequence(f;a), ifthenelse: if b then t else f fi , le: A

B, so_lambda:

x.t[x], implies: P

Q, btrue: tt, not:

A, false: False, bfalse: ff, exists:

x:A. B[x], bool:

, prop:

, so_apply: x[s], unit: Unit, uimplies: b supposing a, assert:

b, uiff: uiff(P;Q), and: P

Q, bnot:

b, or: P

Q, sq_type: SQType(T), guard: {T}, it:

Lemmas : lt_int_wf, subtype_rel_set_simple, le_wf, length_wf, bool_wf, eqtt_to_assert, assert_of_lt_int, select_wf, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, Error :assert-bnot, less_than_wf, Error :zero-le-nat, Error :list_wf, nat_wf
\mforall{}[T:Type]. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mforall{}a:T List. (shifted-sequence(f;a) \mmember{} \mBbbN{} {}\mrightarrow{} T) Date html generated: 2013_03_20-AM-10_36_53 Last ObjectModification: 2013_03_11-PM-07_27_58 Home Index