Buffer: não é indutivo

-

-

-

-

A seguir: Buffer: é indutivo Acima: Variáveis Auxiliares Anterior: Buffer com variáveis auxiliares

Buffer: $P\equiv consumed \leq produced$ não é indutivo

Claramente P é válido inicialmente.

Comando	Prova
$\gamma_{1}$ e $\gamma_{3}$	evidente, pois consumed' = consumed e produced' = produced.
$\gamma_{4}$	Temos $consumed \leq produced$ , consumed' =consumed e produced' = produced + product. Portanto, $consumed' \leq produced'$ .
$\gamma_{2}$	Temos $consumed \leq produced$ , produced' = produced mas consumed' = consumed + buffer.head().

Problema: P não é indutivo!

Osvaldo Carvalho

-

-