Nuprl Lemma : assert-lg-is-source
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[i:ℕlg-size(g)]. uiff(↑lg-is-source(g;i);∀[j:ℕlg-size(g)]. (¬lg-edge(g;j;i)))
Proof
Definitions occuring in Statement :
lg-is-source: lg-is-source(g;i),
lg-edge: lg-edge(g;a;b),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
int_seg: {i..j-},
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
not: ¬A,
natural_number: $n,
universe: Type
Lemmas :
lt_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_lt_int,
list_wf,
assert_elim,
null_wf3,
subtype_rel_list,
top_wf,
member-implies-null-eq-bfalse,
btrue_neq_bfalse,
l_member_wf,
assert_wf,
assert_of_null,
assert_witness,
uall_wf,
not_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
less_than_wf,
false_wf,
lg-in-edges_wf,
int_seg_wf,
lg-size_wf,
nat_wf,
labeled-graph_wf,
list-cases,
product_subtype_list,
cons_member
Latex:
\mforall{}[T:Type]. \mforall{}[g:LabeledGraph(T)]. \mforall{}[i:\mBbbN{}lg-size(g)].
uiff(\muparrow{}lg-is-source(g;i);\mforall{}[j:\mBbbN{}lg-size(g)]. (\mneg{}lg-edge(g;j;i)))
Date html generated:
2015_07_22-PM-00_29_32
Last ObjectModification:
2015_01_28-PM-11_33_07
Home
Index