Nuprl Lemma : partition-mesh-nil

[I:Top]. (partition-mesh(I;[]) |I|)


Proof




Definitions occuring in Statement :  partition-mesh: partition-mesh(I;p) i-length: |I| nil: [] uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] partition-mesh: partition-mesh(I;p) full-partition: full-partition(I;p) frs-mesh: frs-mesh(p) all: x:A. B[x] member: t ∈ T top: Top append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] lt_int: i <j subtract: m ifthenelse: if then else fi  bfalse: ff rmaximum: rmaximum(n;m;k.x[k]) select: L[n] cons: [a b] i-length: |I|
Lemmas referenced :  length_of_cons_lemma list_ind_nil_lemma length_of_nil_lemma primrec0_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation sqequalRule cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis

Latex:
\mforall{}[I:Top].  (partition-mesh(I;[])  \msim{}  |I|)



Date html generated: 2016_05_18-AM-08_56_39
Last ObjectModification: 2015_12_27-PM-11_37_32

Theory : reals


Home Index