======================================================================
ENUNCIADO:

Sejam:

  * IF: if    a > b -> a, b := b, a
           [] b > c -> b, c := c, b
        fi

  * I: x,y,z ∈ Z && multiset{a,b,c} = multiset{x,y,z}

  * BB: a > b || b > c

  * t = t(a,b,c) = (a−b) + (b−c) + |a| + |b| + |c|

                 = a − c + |a| + |b| + |c|

Assim sendo, prove:

  * VC2: I && BB ==> wdec(IF, t)

======================================================================
RESPOSTA:

Pelo teorema 2, temos que mostrar:

  * VC2-1: I && a > b ==> wdec("a, b := b, a", t)

  * VC2-2: I && b > c ==> wdec("b, c := c, b", t)

Para provar VC2-1, calculemos:

  wp("a, b := b, a", t <= t0)

    = wp("a, b := b, a", a − c + |a| + |b| + |c| <= t0)

    = b − c + |b| + |a| + |c| <= t0

Assim, pela definição de wdec, temos:

  wdec("a, b := b, a", t)

       = b − c + |b| + |a| + |c| < t

       = b − c + |b| + |a| + |c| < a − c + |a| + |b| + |c|

    <==> b < a

Portanto, para verificar VC2-1, precisamos provar que

  I && a > b ==> b < a

o que é trivialmente verdadeiro.

De forma análoga, para provar VC2-2, calculemos:

  wp("b, c := c, b", t <= t0)

    = wp("b, c := c, b", a − c + |a| + |b| + |c| <= t0)

    = a − b + |a| + |c| + |b| <= t0

Assim, pela definição de wdec, temos:

  wdec("b, c := c, b", t)

       = a − b + |a| + |c| + |b| < t

       = a − b + |a| + |c| + |b| < a − c + |a| + |b| + |c|

    <==> − b < − c

    <==> b > c

Portanto, para provar VC2-2, precisamos mostrar que

  I && b > c ==> b > c

o que é trivialmente verdadeiro, completando a prova.

======================================================================