Prova:
{ true } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( y >= x ) } { 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 ) ) => ( y >= x ) )Sentenças a serem provadas:
( ( true and not ( y < x ) ) => ( y >= x ) ) ( ( true and ( y < x ) ) => true )