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 = 1 ) or ( a = -1 ) ) } { ( ( a = 0 ) and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( ( a = 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) ) { ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } { ( ( a = 0 ) and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( ( a = 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) { ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) }Sentenças a serem provadas:
( ( ( a = 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) ( ( ( a = 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) )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 = 1 ) or ( a = -1 ) ) } ( ( 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 = 1 ) or ( a = -1 ) ) } { ( not ( b > 0 ) and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( not ( b > 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) ) { ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } { ( not ( b > 0 ) and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( not ( b > 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) { ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) }Sentenças a serem provadas:
( ( a = 0 ) => not ( b > 0 ) ) ( ( not ( b > 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) ( ( not ( b > 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) )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 = 1 ) or ( a = -1 ) ) } ( ( 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 = 1 ) or ( a = -1 ) ) } { ( ( b > 0 ) and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( ( b > 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) ) { ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } { ( ( b > 0 ) and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) } ( ( ( b > 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) { ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( ( a = 1 ) or ( a = -1 ) ) }Sentenças a serem provadas:
( ( a = 0 ) => ( b > 0 ) ) ( ( ( b > 0 ) and not ( b > 0 ) ) => ( ( ( a + 1 ) = 1 ) or ( ( a + 1 ) = -1 ) ) ) ( ( ( b > 0 ) and ( b > 0 ) ) => ( ( ( a - 1 ) = 1 ) or ( ( a - 1 ) = -1 ) ) )