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