Nuprl Lemma : equal_upto_mklist

f,g:

.

n:

. (equal_upto(n;f;g)

(

m:

. ((m

n)

(mklist(m;f) ~ mklist(m;g)))))

Proof

Definitions occuring in Statement : equal_upto: equal_upto(n;f;g), nat:

, le: A

B, all:

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

Q, function: x:A

B[x], sqequal: s ~ t, mklist: mklist(n;f)
Definitions : all:

x:A. B[x], nat:

, implies: P

Q, equal_upto: equal_upto(n;f;g), int_seg: {i..j

}, member: t

T, so_lambda:

x.t[x], lelt: i

j < k, and: P

Q, top: Top, le: A

B, not:

A, false: False, rev_implies: P

Q, iff: P

Q, sq_type: SQType(T), uall:

[x:A]. B[x], uimplies: b supposing a, prop:

, so_apply: x[s], guard: {T}
Lemmas : subtype_base_sq, Error :list_wf, nat_wf, list_subtype_base, set_subtype_base, le_wf, int_subtype_base, all_wf, int_seg_wf, equal_wf, subtype_rel_sets, lelt_wf, list_extensionality, mklist_wf, subtype_rel_dep_function, less_than_wf, length_wf, mklist_length, mklist_select
\mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}n:\mBbbN{}. (equal\_upto(n;f;g) {}\mRightarrow{} (\mforall{}m:\mBbbN{}. ((m \mleq{} n) {}\mRightarrow{} (mklist(m;f) \msim{} mklist(m;g))))) Date html generated: 2013_03_20-AM-10_39_04 Last ObjectModification: 2013_03_17-PM-06_00_35 Home Index