Prova:
{ true } [atribui(a, num(5)), skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [atribui(a, num(5))] { true } { true } [skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [skip] { true } { true } [atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [atribui(b, num(6))] { true } ( true => ( ( b + a ) = 11 ) )Sentenças a serem provadas:
( true => ( ( b + a ) = 11 ) )Prova:
{ true } [atribui(a, num(5)), skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [atribui(a, num(5))] { true } { true } [skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [skip] { true } { true } [atribui(b, num(6))] { ( ( b + a ) = 11 ) } ( true => ( ( 6 + a ) = 11 ) ) { ( ( 6 + a ) = 11 ) } [atribui(b, num(6))] { ( ( b + a ) = 11 ) }Sentenças a serem provadas:
( true => ( ( 6 + a ) = 11 ) )Prova:
{ true } [atribui(a, num(5)), skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { true } [atribui(a, num(5))] { ( ( 6 + a ) = 11 ) } ( true => ( ( 6 + 5 ) = 11 ) ) { ( ( 6 + 5 ) = 11 ) } [atribui(a, num(5))] { ( ( 6 + a ) = 11 ) } { ( ( 6 + a ) = 11 ) } [skip, atribui(b, num(6))] { ( ( b + a ) = 11 ) } { ( ( 6 + a ) = 11 ) } [skip] { ( ( 6 + a ) = 11 ) } { ( ( 6 + a ) = 11 ) } [atribui(b, num(6))] { ( ( b + a ) = 11 ) }Sentenças a serem provadas:
( true => ( ( 6 + 5 ) = 11 ) )