Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( y >= 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } { ( ( y = 0 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) ) { ( ( y + 1 ) = 0 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } ( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( y >= 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } ( ( y = 0 ) => ( y <= 10 ) ) { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } { ( ( y <= 10 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) { ( ( y + 1 ) <= 10 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( ( y = 0 ) and not ( y < 10 ) ) ) ( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( y = 0 ) => ( y <= 10 ) ) ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( ( y = 0 ) and not ( y < 10 ) ) ) ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( y >= 0 ) } ( ( y = 0 ) => ( y <= 10 ) ) { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( y >= 0 ) } { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } { ( ( y <= 10 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) { ( ( y + 1 ) <= 10 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( y = 0 ) => ( y <= 10 ) ) ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } ( ( y = 0 ) => ( y <= 10 ) ) { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } { ( ( y <= 10 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) { ( ( y + 1 ) <= 10 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } { ( ( y <= 10 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( ( y <= 10 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } { ( ( ( y <= 10 ) and not ( y < 10 ) ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( ( y <= 10 ) and not ( y < 10 ) ) } ( ( ( ( y <= 10 ) and not ( y < 10 ) ) and ( y > 0 ) ) => ( ( ( y - 1 ) <= 10 ) and not ( ( y - 1 ) < 10 ) ) ) { ( ( ( y - 1 ) <= 10 ) and not ( ( y - 1 ) < 10 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( ( y <= 10 ) and not ( y < 10 ) ) } ( ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( ( y <= 10 ) and not ( y < 10 ) ) and ( y > 0 ) ) => ( ( ( y - 1 ) <= 10 ) and not ( ( y - 1 ) < 10 ) ) ) ( ( y = 0 ) => ( y <= 10 ) ) ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } ( ( y = 0 ) => ( y <= 10 ) ) { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } { ( ( y <= 10 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) { ( ( y + 1 ) <= 10 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } { ( ( y <= 10 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( ( y <= 10 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) ) ( ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( ( ( y <= 10 ) and not ( y < 10 ) ) and not ( y > 0 ) ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) ( ( y = 0 ) => ( y <= 10 ) ) ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } ( ( y = 0 ) => ( y <= 10 ) ) { ( y <= 10 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y <= 10 ) and not ( y < 10 ) ) } { ( ( y <= 10 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) ) { ( ( y + 1 ) <= 10 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y <= 10 ) } { ( ( y <= 10 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } ( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( y <= 10 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) ( ( y = 0 ) => ( y <= 10 ) ) ( ( ( y <= 10 ) and ( y < 10 ) ) => ( ( y + 1 ) <= 10 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } { ( ( y = 0 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) ) { ( ( y + 1 ) = 0 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } { ( ( y = 0 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( ( y = 0 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } { ( ( ( y = 0 ) and not ( y < 10 ) ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( ( y = 0 ) and not ( y < 10 ) ) } ( ( ( ( y = 0 ) and not ( y < 10 ) ) and ( y > 0 ) ) => ( ( ( y - 1 ) = 0 ) and not ( ( y - 1 ) < 10 ) ) ) { ( ( ( y - 1 ) = 0 ) and not ( ( y - 1 ) < 10 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( ( y = 0 ) and not ( y < 10 ) ) } ( ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( ( y = 0 ) and not ( y < 10 ) ) and ( y > 0 ) ) => ( ( ( y - 1 ) = 0 ) and not ( ( y - 1 ) < 10 ) ) ) ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } { ( ( y = 0 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) ) { ( ( y + 1 ) = 0 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } { ( ( y = 0 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( ( y = 0 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } ( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) ) ( ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( ( ( y = 0 ) and not ( y < 10 ) ) and not ( y > 0 ) ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) )Prova:
{ ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))]), while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y = 0 ) } [while(expBool(menor, ide(y), num(10)), [atribui(y, expInt(soma, ide(y), num(1)))])] { ( ( y = 0 ) and not ( y < 10 ) ) } { ( ( y = 0 ) and ( y < 10 ) ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) ) { ( ( y + 1 ) = 0 ) } [atribui(y, expInt(soma, ide(y), num(1)))] { ( y = 0 ) } { ( ( y = 0 ) and not ( y < 10 ) ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } ( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( y = 0 ) } { ( y >= 0 ) } [while(expBool(maior, ide(y), num(0)), [atribui(y, expInt(menos, ide(y), num(1)))])] { ( ( y >= 0 ) and not ( y > 0 ) ) } { ( ( y >= 0 ) and ( y > 0 ) ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) { ( ( y - 1 ) >= 0 ) } [atribui(y, expInt(menos, ide(y), num(1)))] { ( y >= 0 ) } ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) )Sentenças a serem provadas:
( ( ( y = 0 ) and not ( y < 10 ) ) => ( y >= 0 ) ) ( ( ( y >= 0 ) and not ( y > 0 ) ) => ( y = 0 ) ) ( ( ( y >= 0 ) and ( y > 0 ) ) => ( ( y - 1 ) >= 0 ) ) ( ( ( y = 0 ) and ( y < 10 ) ) => ( ( y + 1 ) = 0 ) )