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

Sentenças a serem provadas:

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

Sentenças a serem provadas:

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

Sentenças a serem provadas:

( ( a > 0 ) => ( b > 0 ) ) ( ( ( b > 0 ) and not ( b > 0 ) ) => ( ( ( b > 0 ) => ( ( a + 1 ) >= 0 ) ) and ( ( b <= 0 ) => ( ( a + 1 ) > 1 ) ) ) ) ( ( ( b > 0 ) and ( b > 0 ) ) => ( ( ( b > 0 ) => ( ( a - 1 ) >= 0 ) ) and ( ( b <= 0 ) => ( ( a - 1 ) > 1 ) ) ) )