Prova:

{ true } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { true } { true } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( true and not ( y < x ) ) } { ( true and ( y < x ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { true } ( ( true and ( y < x ) ) => true ) { true } [atribui(y, expInt(soma, ide(y), num(1)))] { true } ( ( true and not ( y < x ) ) => true )

Sentenças a serem provadas:

( ( true and not ( y < x ) ) => true ) ( ( true and ( y < x ) ) => true )