Nuprl Lemma : list-in-fin_spr_unfold

B:

List

.

a:

List.

s:

. (

(a @ [s]

fspr(B))

(

(a

fspr(B)))

(s

(B a)))

Proof

Definitions occuring in Statement : list-in-fin_spr: (a

fspr(B)), append: as @ bs, assert:

b, nat:

, le: A

B, all:

x:A. B[x], iff: P

Q, and: P

Q, apply: f a, function: x:A

B[x]
Definitions : all:

x:A. B[x], exists:

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

T, assert:

b, iff: P

Q, ifthenelse: if b then t else f fi , and: P

Q, bfalse: ff, false: False, implies: P

Q, rev_implies: P

Q, top: Top, nat:

, band: p

q, prop:

, so_lambda:

x.t[x], btrue: tt, uall:

[x:A]. B[x], sq_type: SQType(T), uimplies: b supposing a, uiff: uiff(P;Q), guard: {T}, bool:

, so_apply: x[s], unit: Unit, it:

Lemmas : base_sq, Error :list_wf, nat_wf, list-in-fin_spr_unfold, append_wf, Error :cons_wf, Error :nil_wf, subtype_base_sq, bool_subtype_base, iff_imp_equal_bool, eq_int_wf, length_wf, bfalse_wf, length_nil, non_neg_length, length_wf_nil, length_wf_nat, length_cons, length_append, subtype_rel_list, top_wf, subtype_top, assert_of_eq_int, assert_wf, iff_wf, equal_wf, Error :last_append_singleton, Error :firstn_append_front_singleton, list-in-fin_spr_wf, le_wf, subtype_rel_set_simple, bool_wf, eqtt_to_assert, le_int_wf, iff_transitivity, iff_weakening_uiff, assert_of_band, assert_of_le_int
\mforall{}B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}a:\mBbbN{} List. \mforall{}s:\mBbbN{}. (\muparrow{}(a @ [s] \mmember{} fspr(B)) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}(a \mmember{} fspr(B))) \mwedge{} (s \mleq{} (B a))) Date html generated: 2013_03_20-AM-10_35_17 Last ObjectModification: 2013_03_11-PM-01_03_05 Home Index