Nuprl Lemma : lg-size-remove

[T:Type].

[g:LabeledGraph(T)].

[x:

lg-size(g)]. (lg-size(lg-remove(g;x)) = (lg-size(g) - 1))

Proof not projected

Definitions occuring in Statement : lg-remove: lg-remove(g;n), lg-size: lg-size(g), labeled-graph: LabeledGraph(T), int_seg: {i..j

}, uall:

[x:A]. B[x], subtract: n - m, natural_number: $n, int:

, universe: Type, equal: s = t
Definitions : top: Top, member: t

T, lg-remove: lg-remove(g;n), lg-size: lg-size(g), uall:

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

Q, not:

A, and: P

Q, le: A

B, int_iseg: {i...j}, rev_implies: P

Q, iff: P

Q, true: True, squash:

T, nat:

, int_seg: {i..j

}, labeled-graph: LabeledGraph(T), prop:

, lelt: i

j < k, uimplies: b supposing a
Lemmas : labeled-graph_wf, nat_wf, lg-size_wf, int_seg_wf, length-append, nth_tl_wf, firstn_wf, top_wf, append_wf, length-map-sq, le_wf, and_wf, length_nth_tl, add_functionality_wrt_eq, length_firstn, true_wf, squash_wf, member_wf

\mforall{}[T:Type]. \mforall{}[g:LabeledGraph(T)]. \mforall{}[x:\mBbbN{}lg-size(g)]. (lg-size(lg-remove(g;x)) = (lg-size(g) - 1)) Date html generated: 2012_01_23-PM-12_36_50 Last ObjectModification: 2011_12_20-PM-12_47_04 Home Index