00. ABREVIAÇÃO: CFC -> componente(s) fortemente conexa(s).

01. ALGORITMO:

------------------------------------------------------------
Algoritmo: Comp_Fort_Conexas
Entrada: grafo direcionado G = (V,E)
Saída: um conjunto de subconjuntos de V
---------------------------------------
01. Compute o grafo direcionado G' = (V,E') tal que
      (u,v) \in E' <=> (v,u) \in E.
02. O := lista vazia
03. para cada vértice v de G
04. | cor[v] := branco
05. para cada vértice v de G
06. | se cor[v] = branco
07. | | BP_Ordem(G',v,cor,O)
08. CFC := conjunto vazio
09. para cada vértice v de G
10. | cor[v] := branco
11. para cada vértice v da lista O
12. | se cor[v] = branco
13. | | C := conjunto vazio
14. | | BP_Comp(G,v,cor,C)
15. | | CFC := CFC U {C}
16. retorne CFC
------------------------------------------------------------

------------------------------------------------------------
Algoritmo: BP_Ordem
Entrada: (1) grafo direcionado G = (V,E)
         (2) vértice u de G
         (3) informação cor[v] para cada vértice v de G
         (4) lista O de vértices de G
Saída: nada
-------------------------------------------------------
01. cor[u] := cinza
02. para cada aresta (u,v) \in E
03. | se cor[v] = branco
04. | | BP_Ordem(G,v,cor,O)
05. cor[u] := preto
06. insira u no início da lista O
------------------------------------------------------------

------------------------------------------------------------
Algoritmo: BP_Comp
Entrada: (1) grafo direcionado G = (V,E)
         (2) vértice u de G
         (3) informação cor[v] para cada vértice v de G
         (4) conjunto C
Saída: nada
-------------------------------------------------------
01. cor[u] := cinza
02. C := C U {u}
03. para cada aresta (u,v) \in E
04. | se cor[v] = branco
05. | | BP_Comp(G,v,cor,C)
06. cor[u] := preto
------------------------------------------------------------


02. LEMA: se vértices u e u' pertencem respectivamente a componentes fortemente conexas C e C' distintas de G, e se existe caminho de u a u' em G, então não existe caminho de u' a u em G.

===================================================
----------------- PROVA DO LEMA 2 -----------------
Suponha, por absurdo, que existe caminho de u' a u em G. Logo, como também existe caminho de u a u', então u e u' pertencem à mesma CFC, uma contradição com a suposição do enunciado. Logo, não pode existir caminho de u' a u, CQD.
----------------- PROVA DO LEMA 2 -----------------
===================================================


03. LEMA: se C é uma CFC de G' e u é o primeiro vértice de C a ser descoberto pela primeira busca em profundidade executada em Comp_Fort_Conexas, então u é também primeiro vértice de C na lista O computada pelo algoritmo.

===================================================
----------------- PROVA DO LEMA 3 -----------------
Se C é unitária, então o resultado vale por vacuidade, CQD.
Se C não é unitária, seja v outro vértice de C. Como u é o primeiro vértice de C a ser descoberto pela busca, e como u e v pertencem à mesma CFC, então, no momento em que u é descoberto, há um caminho de vértices brancos de u a v; logo, pelo teorema do caminho branco, v é descendente de u na busca, o que implica que a visita de v é terminada antes da visita de u, e portanto que u é inserido em O depois de v, e portanto que u ocorre antes de v em O, CQD.
----------------- PROVA DO LEMA 3 -----------------
===================================================


04. LEMA: se u e u' são respectivamente os primeiros vértices de componentes fortemente conexas C e C' distintas de G a aparecerem na lista O do algoritmo "Comp_Fort_Conexas", e se existe caminho de u a u' em G, então u' ocorre antes de u na lista O.

===================================================
----------------- PROVA DO LEMA 4 -----------------
Primeiramente observe que, pelo lema 2, não existe caminho de u' a u em G. Logo, também não existe caminho de u a u' em G'.

Consideremos agora os casos possíveis:

Caso 1: u é descoberto primeiro que u' na primeira busca em profundidade do algoritmo Comp_Fort_Conexas.
Nesse caso, como não existe caminho de u a u' em G', então u' não é descendente de u na primeira busca em profundidade, o que, pelo teorema dos parênteses, implica que u' é pintado de preto depois de u, e portanto que u' ocorre antes de u em O, CQD.

Caso 2: u' é descoberto primeiro que u na primeira busca em profundidade do algoritmo Comp_Fort_Conexas.
Seja então um caminho qualquer de u' a u em G'; nós mostraremos a seguir que todos os vértices desse caminho estão brancos no momento em que u' é descoberto.
De fato, quando u' é descoberto, u' está branco, e, como u' é descoberto antes de u, então u também o está.
Suponha então, por absurdo, que há vértices não brancos nesse caminho quando u' é descoberto. Seja então w o último vértice desse caminho que não está branco quando u' é descoberto. Observe que, quando u' é descoberto, w não pode estar preto, pois o sucessor de w no caminho está, pela escolha de w, necessariamente branco, e vértices pretos não podem ter vizinhos (de saída) brancos na busca em profundidade. Logo, quando u' é descoberto, w está cinza, e portanto w é ancestral de u' na busca. Logo, existe um caminho orientado de w a u' em G', e, como w está no caminho orientado de u' a u em G', então w pertence à mesma CFC de u'. Logo, u' não é o primeiro vértice de C' a ser descoberto pela busca. Entretanto, como u' é o primeiro vértice de C' a aparecer em O, então, pelo lema 3, u' é o primeiro vértice de C' a ser descoberto na busca, um absurdo com a conclusão anterior. Logo, nós concluímos que, quando u' é descoberto, todos os vértices do caminho em questão de u' a u estão brancos.
Logo, pelo teorema do caminho branco, u é descendente de u' na busca, e portanto u' é pintado de preto depois de u, e portanto u' ocorre antes de u na lista O, CQD.
----------------- PROVA DO LEMA 4 -----------------
===================================================


05. TEOREMA: em cada iteração do laço da linha 11 do algoritmo Comp_Fort_Conexas, os elementos de CFC são componentes fortemente conexas de G.

======================================================
----------------- PROVA DO TEOREMA 5 -----------------
Nós mostraremos que a afirmação "os elementos de CFC são componentes fortemente conexas de G" é um invariante do laço em questão.

* Base: vale por vacuidade, já que CFC é vazio.

* Passo: suponhamos que o resultado vale no início de uma iteração; temos que mostrar que ele vale ao fim da iteração em questão.
Observe que, pela hipótese, todo elemento que está em CFC ao final da iteração e que já estava em CFC no início da iteração é uma componente fortemente conexa de G. Logo, pelo algoritmo, o que ainda há para se mostrar é que, se, ao final da iteração, CFC possui um elemento adicional C, então C é uma componente fortemente conexa de G.
De fato, suponha que um conjunto C é adicionado a CFC durante a iteração em questão.
Nós mostraremos que o conjunto C é exatamente a componente fortemente conexa do vértice v que estava branco no início da iteração. Nós o faremos em dois passos:

* Afirmação 1: todo vértice da componente fortemente conexa de v está branco no início da iteração.
A veracidade dessa afirmação segue do fato de que todo vértice que não está branco no início da iteração já pertence a algum dos conjuntos de CFC, e, nesse caso, se algum dos elementos da componente fortemente conexa de v não estivesse branco, então, pela hipótese, v não estaria branco no início da iteração, um absurdo.

* Afirmação 2: nenhum vértice que não pertence à componente fortemente conexa de v está em C.
Se não há em G componente fortemente conexa distinta da de v, então o resultado vale por vacuidade.
Em caso contrário, seja C' uma componente fortemente conexa de G diferente da de v.
Se não há caminho de v a um vértice de C', então certamente nenhum vértice de C' é incluído em C.
Se, por outro lado, houver caminho de v a um vértice de C', então, pelo lema 4, há um vértice de C' que ocorre antes de v na lista O calculada pelo algoritmo, e portanto todo vértice de C' já está preto quando a busca a partir de v é iniciada. Logo, nenhum vértice de C' é inserido em C, CQD.
----------------- PROVA DO TEOREMA 5 -----------------
======================================================