(i) A é variável proposicional
RANK[A]=0 ≤ 0=G[A]
(ii) A é Falso (bottom)
RANK[Falso]=0 ≤ 0=G[Falso]
Passo Indutivo:
(i) A é ~B
Hipótese Indutiva: RANK[B] ≤ G[B]
Mostrar que: RANK[~B] ≤ G[~B]
(ii) A é (B!C)
Hipóteses Indutivas: RANK[B] ≤ G[B] e RANK[C] ≤ G[C]
Mostrar que: RANK[(B!C)] ≤ G[(B!C)]
Cálculos:
RANK[B] ≤ G[B]
RANK[B]+1 ≤ G[B]+1
RANK[~B] ≤ G[~B]
RANK[B] ≤ G[B]
RANK[C] ≤ G[C]
RANK[B]+RANK[C] ≤ G[B]+G[C]
MAX[RANK[B], RANK[C]] ≤ G[B]+G[C]
MAX[RANK[B], RANK[C]]+1 ≤ G[B]+G[C]+1
RANK[(B!C)] ≤ G[(B!C)]
.
.
