Prova:
{ true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { true } { ( true and ( x > 0 ) ) } [atribui(x, num(1))] { true } ( ( true and ( x > 0 ) ) => true ) { true } [atribui(x, num(1))] { true } { ( true and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { true } ( ( true and not ( x > 0 ) ) => true ) { true } [atribui(x, menos(num(1)))] { true }Sentenças a serem provadas:
( ( true and not ( x > 0 ) ) => true ) ( ( true and ( x > 0 ) ) => true )Prova:
{ true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { true } ( true => not ( x > 0 ) ) { not ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { true } { ( not ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { true } ( ( not ( x > 0 ) and ( x > 0 ) ) => true ) { true } [atribui(x, num(1))] { true } { ( not ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { true } ( ( not ( x > 0 ) and not ( x > 0 ) ) => true ) { true } [atribui(x, menos(num(1)))] { true }Sentenças a serem provadas:
( true => not ( x > 0 ) ) ( ( not ( x > 0 ) and not ( x > 0 ) ) => true ) ( ( not ( x > 0 ) and ( x > 0 ) ) => true )Prova:
{ true } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { true } ( true => ( x > 0 ) ) { ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1))], [atribui(x, menos(num(1)))])] { true } { ( ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { true } ( ( ( x > 0 ) and ( x > 0 ) ) => true ) { true } [atribui(x, num(1))] { true } { ( ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { true } ( ( ( x > 0 ) and not ( x > 0 ) ) => true ) { true } [atribui(x, menos(num(1)))] { true }Sentenças a serem provadas:
( true => ( x > 0 ) ) ( ( ( x > 0 ) and not ( x > 0 ) ) => true ) ( ( ( x > 0 ) and ( x > 0 ) ) => true )