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 ) )