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