Prova:

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

Sentenças a serem provadas:

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

Prova:

{ true } [while(true, [while(true, [skip])])] { true } { true } [while(true, [while(true, [skip])])] { ( true and not true ) } { ( true and true ) } [while(true, [skip])] { true } { ( true and true ) } [while(true, [skip])] { ( ( true and true ) and not true ) } ( ( true and true ) => true ) { true } [while(true, [skip])] { ( ( true and true ) and not 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 and true ) and not true ) ) ( ( ( true and true ) and not true ) => true ) ( ( true and not true ) => true )

Sentenças a serem provadas:

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

Prova:

{ true } [while(true, [while(true, [skip])])] { true } { true } [while(true, [while(true, [skip])])] { ( true and not true ) } { ( true and true ) } [while(true, [skip])] { true } ( ( true and true ) => true ) { 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 ) ( ( true and not true ) => true )

Sentenças a serem provadas:

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