Prova:

{ true } [atribui(A, num(5))] { ( ( A = 5 ) and not ( A <> 5 ) ) } { true } [atribui(A, num(5))] { true } ( true => ( ( A = 5 ) and not ( A <> 5 ) ) )

Sentenças a serem provadas:

( true => ( ( A = 5 ) and not ( A <> 5 ) ) )

Prova:

{ true } [atribui(A, num(5))] { ( ( A = 5 ) and not ( A <> 5 ) ) } ( true => ( ( 5 = 5 ) and not ( 5 <> 5 ) ) ) { ( ( 5 = 5 ) and not ( 5 <> 5 ) ) } [atribui(A, num(5))] { ( ( A = 5 ) and not ( A <> 5 ) ) }

Sentenças a serem provadas:

( true => ( ( 5 = 5 ) and not ( 5 <> 5 ) ) )