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 ) ) )