Prova:

{ ( x = 3 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))], [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))])] { ( x = 2 ) } { ( ( x = 3 ) and ( x > 0 ) ) } [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( ( x = 3 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } ( ( ( x = 3 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) ) { ( ( 1 + 1 ) = 2 ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } { ( ( x + 1 ) = 2 ) } [atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( ( x = 3 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) } { ( ( x = 3 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } ( ( ( x = 3 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) { ( ( - 1 - 1 ) = 2 ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } { ( ( x - 1 ) = 2 ) } [atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) }

Sentenças a serem provadas:

( ( ( x = 3 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) ( ( ( x = 3 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) )

Prova:

{ ( x = 3 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))], [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))])] { ( x = 2 ) } ( ( x = 3 ) => not ( x > 0 ) ) { not ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))], [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))])] { ( x = 2 ) } { ( not ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( not ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } ( ( not ( x > 0 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) ) { ( ( 1 + 1 ) = 2 ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } { ( ( x + 1 ) = 2 ) } [atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( not ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) } { ( not ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) { ( ( - 1 - 1 ) = 2 ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } { ( ( x - 1 ) = 2 ) } [atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) }

Sentenças a serem provadas:

( ( x = 3 ) => not ( x > 0 ) ) ( ( not ( x > 0 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) ( ( not ( x > 0 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) )

Prova:

{ ( x = 3 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))], [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))])] { ( x = 2 ) } ( ( x = 3 ) => ( x > 0 ) ) { ( x > 0 ) } [if(expBool(maior, ide(x), num(0)), [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))], [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))])] { ( x = 2 ) } { ( ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1)), atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( ( x > 0 ) and ( x > 0 ) ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } ( ( ( x > 0 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) ) { ( ( 1 + 1 ) = 2 ) } [atribui(x, num(1))] { ( ( x + 1 ) = 2 ) } { ( ( x + 1 ) = 2 ) } [atribui(x, expInt(soma, ide(x), num(1)))] { ( x = 2 ) } { ( ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1))), atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) } { ( ( x > 0 ) and not ( x > 0 ) ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } ( ( ( x > 0 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) { ( ( - 1 - 1 ) = 2 ) } [atribui(x, menos(num(1)))] { ( ( x - 1 ) = 2 ) } { ( ( x - 1 ) = 2 ) } [atribui(x, expInt(menos, ide(x), num(1)))] { ( x = 2 ) }

Sentenças a serem provadas:

( ( x = 3 ) => ( x > 0 ) ) ( ( ( x > 0 ) and not ( x > 0 ) ) => ( ( - 1 - 1 ) = 2 ) ) ( ( ( x > 0 ) and ( x > 0 ) ) => ( ( 1 + 1 ) = 2 ) )