Nuprl Lemma : gammaFIM_equi_length

g,h:

List

.
(spr(g)

(

a:

List. (((g a) = 0)

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

((g []) = 0)

(

f:

.

x:

. (x ~ ||gammaFIM(mklist(x;f);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, sqequal: s ~ t, equal: s = t, mklist: mklist(n;f)
Definitions : all:

x:A. B[x], nat:

, implies: P

Q, member: t

T, le: A

B, prop:

, so_lambda:

x.t[x], rev_implies: P

Q, iff: P

Q, int_seg: {i..j

}, and: P

Q, not:

A, false: False, top: Top, sq_type: SQType(T), uall:

[x:A]. B[x], uimplies: b supposing a, so_apply: x[s], guard: {T}, lelt: i

j < k
Lemmas : subtype_base_sq, nat_wf, set_subtype_base, le_wf, subtype_rel_set_simple, int_subtype_base, gammaFIM_equi_length, mklist_wf, subtype_rel_dep_function, int_seg_wf, subtype_rel_sets, lelt_wf, subtype_rel_weakening, ext-eq_weakening, equal_wf, Error :nil_wf, all_wf, Error :list_wf, append_wf, Error :cons_wf, spr_wf, mklist_length
\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{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}x:\mBbbN{}. (x \msim{} ||gammaFIM(mklist(x;f);g;h)||))) Date html generated: 2013_03_20-AM-10_33_23 Last ObjectModification: 2013_03_08-PM-11_42_29 Home Index