Nuprl Lemma : gammaFIM_equi

g,h:

List

.
(spr(g)

(

a:

List. (((g a) = 0)

((g (a @ [h a])) = 0)))

((g []) = 0)

(

L:

List. (||L|| = ||gammaFIM(L;g;h)||)))

Proof

Definitions occuring in Statement : gammaFIM: gammaFIM(a;g;h), length: ||as||, append: as @ bs, nat:

, all:

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

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

B[x], natural_number: $n, equal: s = t
Definitions : all:

x:A. B[x], nat:

, implies: P

Q, gammaFIM: gammaFIM(a;g;h), member: t

T, prop:

, le: A

B, not:

A, false: False, so_lambda:

x.t[x], length: ||as||, ifthenelse: if b then t else f fi , btrue: tt, bfalse: ff, exists:

x:A. B[x], uall:

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

, guard: {T}, unit: Unit, uimplies: b supposing a, assert:

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

Q, bnot:

b, or: P

Q, sq_type: SQType(T), true: True, it:

Lemmas : Error :list_wf, nat_wf, equal_wf, Error :nil_wf, le_wf, all_wf, append_wf, Error :cons_wf, spr_wf, Error :list_ind_reverse_wf_dependent, eq_int_wf, subtype_rel_set_simple, bool_wf, eqtt_to_assert, assert_of_eq_int, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, Error :assert-bnot, neg_assert_of_eq_int, length_wf_nat, length_wf, length_nil, non_neg_length, length_wf_nil, length_cons, length_append, subtype_rel_list, top_wf, subtype_top, Error :list_ind_reverse_wf
\mforall{}g,h:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} ((g (a @ [h a])) = 0))) {}\mRightarrow{} ((g []) = 0) {}\mRightarrow{} (\mforall{}L:\mBbbN{} List. (||L|| = ||gammaFIM(L;g;h)||))) Date html generated: 2013_03_20-AM-10_33_18 Last ObjectModification: 2013_03_08-PM-11_00_10 Home Index