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 ) )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 ) => ( 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 ) ) => ( y = x ) )Sentenças a serem provadas:
( ( ( y < x ) and not ( y < x ) ) => ( y = x ) ) ( ( 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)))])] { ( 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 ) } { ( 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 ) => ( y <= x ) ) ( ( ( y <= x ) and not ( y < x ) ) => ( y = x ) ) ( ( ( y <= x ) and ( y < x ) ) => ( ( y + 1 ) <= x ) )