:: deftheorem defines LexBFS:Update LEXBFS:def 13 :
for G being _finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for n being Nat holds LexBFS:Update (L,v,n) = [((L `1) +* (v .--> ((G .order()) -' n))),((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}))];