Prova:
{ c } [if(expBool(or, expBool(and, ide(a), ide(b)), ide(c)), [atribui(a, true), atribui(b, false)], [atribui(a, neg(expBool(and, ide(b), ide(c))))])] { ( a and not b ) } { ( c and ( ( a and b ) or c ) ) } [atribui(a, true), atribui(b, false)] { ( a and not b ) } { ( c and ( ( a and b ) or c ) ) } [atribui(a, true)] { ( a and not false ) } ( ( c and ( ( a and b ) or c ) ) => ( true and not false ) ) { ( true and not false ) } [atribui(a, true)] { ( a and not false ) } { ( a and not false ) } [atribui(b, false)] { ( a and not b ) } { ( c and not ( ( a and b ) or c ) ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) } ( ( c and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) { ( not ( b and c ) and not b ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) }Sentenças a serem provadas:
( ( c and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) ( ( c and ( ( a and b ) or c ) ) => ( true and not false ) )Prova:
{ c } [if(expBool(or, expBool(and, ide(a), ide(b)), ide(c)), [atribui(a, true), atribui(b, false)], [atribui(a, neg(expBool(and, ide(b), ide(c))))])] { ( a and not b ) } ( c => not ( ( a and b ) or c ) ) { not ( ( a and b ) or c ) } [if(expBool(or, expBool(and, ide(a), ide(b)), ide(c)), [atribui(a, true), atribui(b, false)], [atribui(a, neg(expBool(and, ide(b), ide(c))))])] { ( a and not b ) } { ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true), atribui(b, false)] { ( a and not b ) } { ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true)] { ( a and not false ) } ( ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and not false ) ) { ( true and not false ) } [atribui(a, true)] { ( a and not false ) } { ( a and not false ) } [atribui(b, false)] { ( a and not b ) } { ( not ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) } ( ( not ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) { ( not ( b and c ) and not b ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) }Sentenças a serem provadas:
( c => not ( ( a and b ) or c ) ) ( ( not ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) ( ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and not false ) )Prova:
{ c } [if(expBool(or, expBool(and, ide(a), ide(b)), ide(c)), [atribui(a, true), atribui(b, false)], [atribui(a, neg(expBool(and, ide(b), ide(c))))])] { ( a and not b ) } ( c => ( ( a and b ) or c ) ) { ( ( a and b ) or c ) } [if(expBool(or, expBool(and, ide(a), ide(b)), ide(c)), [atribui(a, true), atribui(b, false)], [atribui(a, neg(expBool(and, ide(b), ide(c))))])] { ( a and not b ) } { ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true), atribui(b, false)] { ( a and not b ) } { ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true)] { ( a and not false ) } ( ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and not false ) ) { ( true and not false ) } [atribui(a, true)] { ( a and not false ) } { ( a and not false ) } [atribui(b, false)] { ( a and not b ) } { ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) } ( ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) { ( not ( b and c ) and not b ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and not b ) }Sentenças a serem provadas:
( c => ( ( a and b ) or c ) ) ( ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and not b ) ) ( ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and not false ) )