Prova:

{ ( x = 1 ) } [if(expBool(igual, ide(x), num(0)), [atribui(x, num(1))])] { ( x = 1 ) } { ( ( x = 1 ) and ( x = 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x = 1 ) and ( x = 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x = 1 ) and not ( x = 0 ) ) => ( x = 1 ) )

Sentenças a serem provadas:

( ( ( x = 1 ) and not ( x = 0 ) ) => ( x = 1 ) ) ( ( ( x = 1 ) and ( x = 0 ) ) => ( 1 = 1 ) )

Prova:

{ ( x = 1 ) } [if(expBool(igual, ide(x), num(0)), [atribui(x, num(1))])] { ( x = 1 ) } ( ( x = 1 ) => not ( x = 0 ) ) { not ( x = 0 ) } [if(expBool(igual, ide(x), num(0)), [atribui(x, num(1))])] { ( x = 1 ) } { ( not ( x = 0 ) and ( x = 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( not ( x = 0 ) and ( x = 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( not ( x = 0 ) and not ( x = 0 ) ) => ( x = 1 ) )

Sentenças a serem provadas:

( ( x = 1 ) => not ( x = 0 ) ) ( ( not ( x = 0 ) and not ( x = 0 ) ) => ( x = 1 ) ) ( ( not ( x = 0 ) and ( x = 0 ) ) => ( 1 = 1 ) )

Prova:

{ ( x = 1 ) } [if(expBool(igual, ide(x), num(0)), [atribui(x, num(1))])] { ( x = 1 ) } ( ( x = 1 ) => ( x = 0 ) ) { ( x = 0 ) } [if(expBool(igual, ide(x), num(0)), [atribui(x, num(1))])] { ( x = 1 ) } { ( ( x = 0 ) and ( x = 0 ) ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x = 0 ) and ( x = 0 ) ) => ( 1 = 1 ) ) { ( 1 = 1 ) } [atribui(x, num(1))] { ( x = 1 ) } ( ( ( x = 0 ) and not ( x = 0 ) ) => ( x = 1 ) )

Sentenças a serem provadas:

( ( x = 1 ) => ( x = 0 ) ) ( ( ( x = 0 ) and not ( x = 0 ) ) => ( x = 1 ) ) ( ( ( x = 0 ) and ( x = 0 ) ) => ( 1 = 1 ) )