Prova:
{ ( ( 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 b ) } { ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true), atribui(b, false)] { ( a and b ) } { ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true)] { ( a and false ) } ( ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and false ) ) { ( true and false ) } [atribui(a, true)] { ( a and false ) } { ( a and false ) } [atribui(b, false)] { ( a and b ) } { ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and b ) } ( ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and b ) ) { ( not ( b and c ) and b ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and b ) }Sentenças a serem provadas:
( ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and b ) ) ( ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and false ) )Prova:
{ ( ( 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 b ) } ( ( ( a and b ) or 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 b ) } { ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true), atribui(b, false)] { ( a and b ) } { ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) } [atribui(a, true)] { ( a and false ) } ( ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and false ) ) { ( true and false ) } [atribui(a, true)] { ( a and false ) } { ( a and false ) } [atribui(b, false)] { ( a and 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 b ) } ( ( not ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => ( not ( b and c ) and b ) ) { ( not ( b and c ) and b ) } [atribui(a, neg(expBool(and, ide(b), ide(c))))] { ( a and b ) }Sentenças a serem provadas:
( ( ( a and b ) or 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 b ) ) ( ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => ( true and false ) )