1. LEMA: se
  (1) G=(V,E) é um grafo direcionado,
  (2) "w" é uma atribuição de pesos reais aos arcos de G tal que G não possui circuitos de peso negativo,
  (3) "a", "b" e "c" são vértices distintos de G, tais que existem caminhos orientados de "a" a "b" e "a" a "c", e além disso tais que (b,c) \in E,
então dist(a,c) <= dist(a,b) + w(b,c).

===========================================================
--------------------- PROVA DO LEMA 1 ---------------------
De fato, seja C um caminho orientado de peso mínimo de "a" a "b".
Logo, w(C) = dist(a,b), onde w(C) é a soma dos pesos dos arcos de C.
São então dois casos:
----------
* Caso 1: "c" não está em C.
Nesse caso, o passeio D que se obtém acrescentando-se "a" ao fim de "C" é um caminho orientado de "a" a "c", cujo peso é w(D) = w(C) + w(b,c) = dist(a,b) + w(b,c). Além disso, como a distância dist(a,c) de "a" a "c" não pode ser maior que o peso de um caminho de "a" a "c", então dist(a,c) <= w(D) = dist(a,b) + w(b,c), CQD.

* Caso 2: "c" está em C.
Nesse caso, como C é um caminho, então "c" ocorre em C exatamente uma vez.
Digamos então que C = <v_1, v_2, ..., v_i, ..., v_k>, onde a = v_1, c = v_i e b = v_k.
Sejam então D = <v_1, v_2, ..., v_i> e E = <v_i, v_{i+1}, ..., v_k, c>.
Observe então que D é um caminho de "a" a "c", e que E é um circuito.
Além disso, pela forma como definimos D e E, temos que
  w(D) + w(E) = w(C) + w(b,c) = dist(a,b) + w(b,c)
  -->  w(D) = dist(a,b) + w(b,c) - w(E)
  -->  w(D) <= dist(a,b) + w(b,c)       (pois w(E) >= 0).
(Observe que w(E) >= 0 porque G não possui circuitos de peso negativo.)
Finalmente, assim como no caso anterior, temos dist(a,c) <= w(D) <= dist(a,b) + w(b,c), CQD.
----------
Logo, em ambos os casos possíveis, temos dist(a,c) <= dist(a,b) + w(b,c), CQD.
--------------------- PROVA DO LEMA 1 ---------------------
===========================================================


2. Algoritmo:

----------------------------------------------------------------------
algoritmo: cam_mín_neg
entrada: (1) grafo direcionado G=(V,E), (2) função "w : E -> R" tal
         que G não tenha circuitos de peso negativo, e (3) "o \in V".
saída: dados "pai" e "d" para cada v \in V.
----------------------------------------------------------------------
01. para cada vértice v de G
02. | d[v] := infinito
03. | pai[v] := nulo
04. d[o] := 0
05. faça n-1 vezes
06. | para cada arco (u,v) \in E
07. | | se d[v] > d[u] + w(u,v)
08. | | | d[v] := d[u] + w(u,v)
09. | | | pai[v] := u
10. retorne "pai" e "d".
----------------------------------------------------------------------


3. LEMA: durante toda a execução do laço da linha 5 do algoritmo 2 acima, vale que:
  (A) Para todo v \in V, se d[v] != infinito, então há caminho orientado de "o" a "v".
  (B) Para todo v \in V, d[v] >= dist(o,v).

===========================================================
--------------------- PROVA DO LEMA 3 ---------------------
Observe primeiramente que as afirmações são válidas imediatamente antes do início do laço em questão:
  (A) O único vértice "v \in V" tal que d[v] != infinito é "o", e <o> é um caminho orientado de "o" a "o", como desejado.
  (B) Ao fim do laço da linha 1, d[v] = infinito para todo v \in V, e, logo após a linha 4, d[o] = 0 >= 0 = dist(o,v), como desejado.

Para concluir a demonstração, nós mostraremos que, para toda execução da linha 8, se as afirmações "A" e "B" são válidas imediatamente antes da execução da linha, então elas também valem logo após a execução da linha.
De fato, sejam "u" e "v" os vértices envolvidos numa certa execução da linha 8.
Logo, após a execução da instrução em questão, o valor de "d[v]" é "d[u] + w(u,v)".
Além disso, como a linha 8 foi executada, então a condição da linha 7 era verdadeira logo antes da execução da linha 8, o que implica que d[u] != infinito.
Provemos agora que as afirmações A e B são verdadeiras após a execução da linha 8:
-----
  (A) A linha 8 apenas altera o campo "d" do vértice "v", e portanto apenas para esse vértice o resultado poderia não valer após a execução da linha 8. De fato, como d[u] != infinito, então d[v] != infinito após a linha 8. Agora, como a afirmação "A" é válida antes da execução da linha 8, então existe um caminho orientado de "o" a "u" em G, e, como há um arco ligando "u" a "v", então há um caminho orientado de "o" a "v", CQD.

  (B) Observe que, como a afirmação "B" é verdadeira logo antes da execução da linha 8, temos que
  d[u] >= dist(o,u).
Além disso, como há caminho de "o" a "u" e de "o" a "v" (conforme demonstração acima do item "A"), então, pelo lema 1,
  dist(o,v) <= dist(o,u) + w(u,v)
  --> dist(o,v) <= d[u] + w(u,v).
A inequação acima implica que, após a execução da linha 8, temos que dist(o,v) <= d[v], CQD.
-----
Logo, as afirmações "A" e "B" são válidas durante toda a execução do laço da linha 5, CQD.
--------------------- PROVA DO LEMA 3 ---------------------
===========================================================