Prova:

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

Sentenças a serem provadas:

( ( ( y <= x ) and not ( y < x ) ) => ( y = x ) ) ( ( ( y <= x ) and ( y < x ) ) => ( ( y + 1 ) <= x ) )