Prova:

{ ( y = x ) } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( x = y ) } { ( 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 ) ) => ( x = y ) )

Sentenças a serem provadas:

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

Prova:

{ ( y = x ) } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( x = y ) } { ( 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 ) => ( 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 ) } [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 ) and not ( y < x ) ) ) ( ( ( y = x ) and not ( y < x ) ) => ( x = y ) )

Sentenças a serem provadas:

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

Prova:

{ ( y = x ) } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( x = y ) } ( ( y = x ) => ( y <= x ) ) { ( y <= x ) } [while(expBool(menor, ide(y), ide(x)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( x = y ) } { ( 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 ) ) => ( x = y ) )

Sentenças a serem provadas:

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