Prova:

{ true } [skip, atribui(a, num(5)), atribui(b, num(6))] { ( b = 5 ) } { true } [skip] { true } { true } [atribui(a, num(5)), atribui(b, num(6))] { ( b = 5 ) } { true } [atribui(a, num(5))] { true } { true } [atribui(b, num(6))] { ( b = 5 ) } { true } [atribui(b, num(6))] { true } ( true => ( b = 5 ) )

Sentenças a serem provadas:

( true => ( b = 5 ) )

Prova:

{ true } [skip, atribui(a, num(5)), atribui(b, num(6))] { ( b = 5 ) } { true } [skip] { true } { true } [atribui(a, num(5)), atribui(b, num(6))] { ( b = 5 ) } { true } [atribui(a, num(5))] { true } { true } [atribui(b, num(6))] { ( b = 5 ) } ( true => ( 6 = 5 ) ) { ( 6 = 5 ) } [atribui(b, num(6))] { ( b = 5 ) }

Sentenças a serem provadas:

( true => ( 6 = 5 ) )