Step
*
1
1
of Lemma
lg-edge-remove
.....equality.....
1. T : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
⊢ ||firstn(i;g) @ nth_tl(i + 1;g)|| ~ lg-size(lg-remove(g;i))
BY
{ (RepUR ``lg-size lg-remove`` 0 THEN RWO "length-map-sq" 0 THEN Auto) }
Latex:
Latex:
.....equality.....
1. T : Type
2. g : LabeledGraph(T)@i
3. i : \mBbbN{}lg-size(g)@i
4. a : \mBbbN{}lg-size(g) - 1@i
5. b : \mBbbN{}lg-size(g) - 1@i
\mvdash{} ||firstn(i;g) @ nth\_tl(i + 1;g)|| \msim{} lg-size(lg-remove(g;i))
By
Latex:
(RepUR ``lg-size lg-remove`` 0 THEN RWO "length-map-sq" 0 THEN Auto)
Home
Index