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