Prova:

{ true } [atribui(x, num(2)), if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { true } [atribui(x, num(2))] { true } { true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { ( true and ( x > 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( true and ( x > 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } { ( true and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( x = 1 ) } ( ( true and not ( x > 0 ) ) => ( - 1 = 1 ) ) { ( - 1 = 1 ) } [atribui(x, menos(num(1)))] { ( x = 1 ) }

Sentenças a serem provadas:

( ( true and not ( x > 0 ) ) => ( - 1 = 1 ) ) ( ( true and ( x > 0 ) ) => ( 1 = 1 ) )

Prova:

{ true } [atribui(x, num(2)), if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { true } [atribui(x, num(2))] { true } { true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } ( true => not ( x > 0 ) ) { not ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { ( not ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( not ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } { ( not ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( x = 1 ) } ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) { ( - 1 = 1 ) } [atribui(x, menos(num(1)))] { ( x = 1 ) }

Sentenças a serem provadas:

( true => not ( x > 0 ) ) ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) ( ( not ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) )

Prova:

{ true } [atribui(x, num(2)), if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { true } [atribui(x, num(2))] { true } { true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } ( true => ( x > 0 ) ) { ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { ( ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } { ( ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( x = 1 ) } ( ( ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) { ( - 1 = 1 ) } [atribui(x, menos(num(1)))] { ( x = 1 ) }

Sentenças a serem provadas:

( true => ( x > 0 ) ) ( ( ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) ( ( ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) )

Prova:

{ true } [atribui(x, num(2)), if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { true } [atribui(x, num(2))] { not ( x > 0 ) } ( true => not ( 2 > 0 ) ) { not ( 2 > 0 ) } [atribui(x, num(2))] { not ( x > 0 ) } { not ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { ( not ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( not ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } { ( not ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( x = 1 ) } ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) { ( - 1 = 1 ) } [atribui(x, menos(num(1)))] { ( x = 1 ) }

Sentenças a serem provadas:

( true => not ( 2 > 0 ) ) ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) ( ( not ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) )

Prova:

{ true } [atribui(x, num(2)), if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { true } [atribui(x, num(2))] { ( x > 0 ) } ( true => ( 2 > 0 ) ) { ( 2 > 0 ) } [atribui(x, num(2))] { ( x > 0 ) } { ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { ( x = 1 ) } { ( ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } { ( ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( x = 1 ) } ( ( ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) { ( - 1 = 1 ) } [atribui(x, menos(num(1)))] { ( x = 1 ) }

Sentenças a serem provadas:

( true => ( 2 > 0 ) ) ( ( ( x > 0 ) and not ( x > 0 ) ) => ( - 1 = 1 ) ) ( ( ( x > 0 ) and ( x > 0 ) ) => ( 1 = 1 ) )