Prova:

{ true } [while(true, [skip])] { true } { true } [while(true, [skip])] { ( true and not true ) } { ( true and true ) } [skip] { true } { ( true and true ) } [skip] { ( true and true ) } ( ( true and true ) => true ) ( ( true and not true ) => true )

Sentenças a serem provadas:

( ( true and not true ) => true ) ( ( true and true ) => true )