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