:: deftheorem Def10 defines AP:Step GLIB_005:def 10 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL holds
( ( AP:NextBestEdges VL = {} implies AP:Step VL = VL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) );