Prova:

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

Sentenças a serem provadas:

( true => ( 11 = ( a + b ) ) )

Prova:

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

Sentenças a serem provadas:

( true => ( 11 = ( a + 6 ) ) )

Prova:

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

Sentenças a serem provadas:

( true => ( 11 = ( 5 + 6 ) ) )