Prova:

{ true } [if(expBool(maior, ide(b), num(0)), [atribui(a, expInt(menos, ide(a), num(1)))], [atribui(a, expInt(soma, ide(a), num(1)))])] { true } { true } [if(expBool(maior, ide(b), num(0)), [atribui(a, expInt(menos, ide(a), num(1)))], [atribui(a, expInt(soma, ide(a), num(1)))])] { ( true and ( b > 0 ) ) } { ( true and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( true and ( b > 0 ) ) } { ( true and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( true and ( b > 0 ) ) } { ( true and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( true and not ( b > 0 ) ) } ( ( true and not ( b > 0 ) ) => ( true and ( b > 0 ) ) ) ( ( true and ( b > 0 ) ) => true )

Sentenças a serem provadas:

( ( true and ( b > 0 ) ) => true ) ( ( true and not ( b > 0 ) ) => ( true and ( b > 0 ) ) )

Prova:

{ true } [if(expBool(maior, ide(b), num(0)), [atribui(a, expInt(menos, ide(a), num(1)))], [atribui(a, expInt(soma, ide(a), num(1)))])] { true } { ( true and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { true } { ( true and ( b > 0 ) ) } [atribui(a, expInt(menos, ide(a), num(1)))] { ( true and ( b > 0 ) ) } ( ( true and ( b > 0 ) ) => true ) { ( true and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { true } { ( true and not ( b > 0 ) ) } [atribui(a, expInt(soma, ide(a), num(1)))] { ( true and not ( b > 0 ) ) } ( ( true and not ( b > 0 ) ) => true )

Sentenças a serem provadas:

( ( true and not ( b > 0 ) ) => true ) ( ( true and ( b > 0 ) ) => true )

Prova:

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

Sentenças a serem provadas:

( true => not ( b > 0 ) ) ( ( not ( b > 0 ) and not ( b > 0 ) ) => true ) ( ( not ( b > 0 ) and ( b > 0 ) ) => true )

Prova:

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

Sentenças a serem provadas:

( true => ( b > 0 ) ) ( ( ( b > 0 ) and not ( b > 0 ) ) => true ) ( ( ( b > 0 ) and ( b > 0 ) ) => true )