Prova:

{ true } [atribui(a, expInt(soma, expInt(soma, ide(b), ide(c)), ide(d)))] { ( a = ( ( c + b ) + d ) ) } { true } [atribui(a, expInt(soma, expInt(soma, ide(b), ide(c)), ide(d)))] { true } ( true => ( a = ( ( c + b ) + d ) ) )

Sentenças a serem provadas:

( true => ( a = ( ( c + b ) + d ) ) )

Prova:

{ true } [atribui(a, expInt(soma, expInt(soma, ide(b), ide(c)), ide(d)))] { ( a = ( ( c + b ) + d ) ) } ( true => ( ( ( b + c ) + d ) = ( ( c + b ) + d ) ) ) { ( ( ( b + c ) + d ) = ( ( c + b ) + d ) ) } [atribui(a, expInt(soma, expInt(soma, ide(b), ide(c)), ide(d)))] { ( a = ( ( c + b ) + d ) ) }

Sentenças a serem provadas:

( true => ( ( ( b + c ) + d ) = ( ( c + b ) + d ) ) )