Nuprl Lemma : lg-label-append
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. ∀[x:ℕlg-size(lg-append(g1;g2))].
(lg-label(lg-append(g1;g2);x) ~ if x <z lg-size(g1) then lg-label(g1;x) else lg-label(g2;x - lg-size(g1)) fi )
Proof
Definitions occuring in Statement :
lg-label: lg-label(g;x),
lg-append: lg-append(g1;g2),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
uall: ∀[x:A]. B[x],
subtract: n - m,
natural_number: $n,
universe: Type,
sqequal: s ~ t
Lemmas :
lg-size_wf,
int_seg_wf,
lg-append_wf,
nat_wf,
labeled-graph_wf,
select-append,
map_wf,
list_wf,
subtype_rel_list,
top_wf,
int_seg_subtype-nat,
false_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,
length-append,
length-map-sq,
subtract_wf,
select-map,
select_wf,
zero-le-nat,
le_wf
Latex:
\mforall{}[T:Type]. \mforall{}[g1,g2:LabeledGraph(T)]. \mforall{}[x:\mBbbN{}lg-size(lg-append(g1;g2))].
(lg-label(lg-append(g1;g2);x) \msim{} if x <z lg-size(g1)
then lg-label(g1;x)
else lg-label(g2;x - lg-size(g1))
fi )
Date html generated:
2015_07_23-AM-11_04_28
Last ObjectModification:
2015_01_28-PM-11_34_38
Home
Index