Prova:

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

Sentenças a serem provadas:

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

Prova:

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

Sentenças a serem provadas:

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

Prova:

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

Sentenças a serem provadas:

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