Nuprl Lemma : lg-acyclic-has-source
∀[T:Type]. ∀g:LabeledGraph(T). (∃i:ℕlg-size(g). (↑lg-is-source(g;i))) supposing (lg-acyclic(g) and 0 < lg-size(g))
Proof
Definitions occuring in Statement :
lg-is-source: lg-is-source(g;i),
lg-acyclic: lg-acyclic(g),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
int_seg: {i..j-},
assert: ↑b,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
natural_number: $n,
universe: Type
Lemmas :
int_seg_wf,
lg-size_wf,
exists_wf,
lg-edge_wf,
all_wf,
nat_wf,
equal_wf,
nat_plus_properties,
lg-connected_wf,
fun_exp_wf,
zero-le-nat,
le_wf,
false_wf,
lelt_wf,
primrec-wf-nat-plus,
nat_plus_wf,
lg-edge-lg-connected,
decidable__le,
not-le-2,
sq_stable__le,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
fun_exp_add1,
lg-connected_transitivity,
subtype_base_sq,
int_subtype_base,
pigeon-hole-implies,
less-iff-le,
decidable__lt,
add-mul-special,
zero-mul,
int_seg_subtype-nat,
sq_stable__equal,
subtract_wf,
less_than_transitivity2,
le_weakening2,
less_than_irreflexivity,
less_than_wf
Latex:
\mforall{}[T:Type]
\mforall{}g:LabeledGraph(T)
(\mexists{}i:\mBbbN{}lg-size(g). (\muparrow{}lg-is-source(g;i))) supposing (lg-acyclic(g) and 0 < lg-size(g))
Date html generated:
2015_07_22-PM-00_29_35
Last ObjectModification:
2015_01_28-PM-11_35_18
Home
Index