Prova:

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

Sentenças a serem provadas:

( ( true and not ( ( a and b ) or c ) ) => true ) ( ( true and ( ( a and b ) or c ) ) => true )

Prova:

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

Sentenças a serem provadas:

( true => not ( ( a and b ) or c ) ) ( ( not ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => true ) ( ( not ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => true )

Prova:

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

Sentenças a serem provadas:

( true => ( ( a and b ) or c ) ) ( ( ( ( a and b ) or c ) and not ( ( a and b ) or c ) ) => true ) ( ( ( ( a and b ) or c ) and ( ( a and b ) or c ) ) => true )