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