{ 
[T:Type]
g:LabeledGraph(T). i,j,a,b:
lg-size(g).
(lg-edge(lg-add(g;i;j);a;b) 
lg-edge(g;a;b) 
((a = i) 
(b = j))) }
{ Proof }
Definitions occuring in Statement :
lg-edge: lg-edge(g;a;b),
lg-add: lg-add(g;a;b),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
int_seg: {i..j
},
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
or: P Q,
and: P Q,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
int_seg: {i..j},
iff: P Q,
lg-edge: lg-edge(g;a;b),
lg-add: lg-add(g;a;b),
or: P Q,
and: P Q,
lg-in-edges: lg-in-edges(g;x),
spreadn: spread3,
ifthenelse: if b then t else f fi ,
pi1: fst(t),
pi2: snd(t),
top: Top,
member: t 
T,
le: A 
B,
lelt: i j < k,
not: 
A,
implies: P Q,
false: False,
prop: 
,
btrue: tt,
rev_implies: P Q,
bfalse: ff,
cand: A c B,
guard: {T},
labeled-graph: LabeledGraph(T),
nat: ,
uimplies: b supposing a,
bool: 
,
unit: Unit,
decidable: Dec(P),
lg-size: lg-size(g),
it: 
Lemmas :
select-mklist,
length_wf_nat,
int_seg_wf,
nat_wf,
le_wf,
select_wf,
eq_int_wf,
bool_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_int,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
l_member_wf,
lg-size_wf,
labeled-graph_wf,
decidable__l_member,
decidable__equal_int,
iff_functionality_wrt_iff,
cons_member
\mforall{}[T:Type]
\mforall{}g:LabeledGraph(T). \mforall{}i,j,a,b:\mBbbN{}lg-size(g).
(lg-edge(lg-add(g;i;j);a;b) \mLeftarrow{}{}\mRightarrow{} lg-edge(g;a;b) \mvee{} ((a = i) \mwedge{} (b = j)))
Date html generated:
2011_08_16-PM-06_39_59
Last ObjectModification:
2011_06_20-AM-01_58_57
Home
Index