### Nuprl Lemma : lg-all-remove

`∀[T:Type]. ∀[P:T ─→ ℙ].  ∀g:LabeledGraph(T). ∀x:ℕlg-size(g).  (∀x∈g.P[x] `⇐⇒` ∀x∈lg-remove(g;x).P[x] ∧ P[lg-label(g;x)])`

Proof

Definitions occuring in Statement :  lg-all: `∀x∈G.P[x]` lg-label: `lg-label(g;x)` lg-remove: `lg-remove(g;n)` lg-size: `lg-size(g)` labeled-graph: `LabeledGraph(T)` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` function: `x:A ─→ B[x]` natural_number: `\$n` universe: `Type`
Lemmas :  int_seg_wf lg-size_wf lg-remove_wf int_seg_subtype-nat false_wf nat_wf all_wf lg-label2_wf labeled-graph_wf int_seg_properties lelt_wf squash_wf true_wf lg-size-remove iff_weakening_equal lg-label-remove subtract_wf lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf decidable__lt less-iff-le condition-implies-le add-associates minus-add minus-one-mul add-swap add-commutes add_functionality_wrt_le le-add-cancel2 decidable__le not-le-2 zero-add add-zero le-add-cancel minus-minus iff_imp_equal_bool btrue_wf assert_wf iff_wf sq_stable__le le-add-cancel-alt bnot_wf not_wf int_subtype_base lg-label_wf and_wf bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot decidable__equal_int not-equal-2

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}g:LabeledGraph(T).  \mforall{}x:\mBbbN{}lg-size(g).    (\mforall{}x\mmember{}g.P[x]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x\mmember{}lg-remove(g;x).P[x]  \mwedge{}  P[lg-label(g;x)])

Date html generated: 2015_07_23-AM-11_04_48
Last ObjectModification: 2015_07_16-AM-10_04_44

Home Index