Prova:

{ true } [atribui(a, num(5)), atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(a, num(5))] { true } { true } [atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(b, num(6))] { true } { true } [atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(c, expInt(soma, ide(a), ide(b)))] { true } ( true => ( ( ( a + b ) + c ) = 22 ) )

Sentenças a serem provadas:

( true => ( ( ( a + b ) + c ) = 22 ) )

Prova:

{ true } [atribui(a, num(5)), atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(a, num(5))] { true } { true } [atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(b, num(6))] { true } { true } [atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } ( true => ( ( ( a + b ) + ( a + b ) ) = 22 ) ) { ( ( ( a + b ) + ( a + b ) ) = 22 ) } [atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) }

Sentenças a serem provadas:

( true => ( ( ( a + b ) + ( a + b ) ) = 22 ) )

Prova:

{ true } [atribui(a, num(5)), atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(a, num(5))] { true } { true } [atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(b, num(6))] { ( ( ( a + b ) + ( a + b ) ) = 22 ) } ( true => ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) ) { ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) } [atribui(b, num(6))] { ( ( ( a + b ) + ( a + b ) ) = 22 ) } { ( ( ( a + b ) + ( a + b ) ) = 22 ) } [atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) }

Sentenças a serem provadas:

( true => ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) )

Prova:

{ true } [atribui(a, num(5)), atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { true } [atribui(a, num(5))] { ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) } ( true => ( ( ( 5 + 6 ) + ( 5 + 6 ) ) = 22 ) ) { ( ( ( 5 + 6 ) + ( 5 + 6 ) ) = 22 ) } [atribui(a, num(5))] { ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) } { ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) } [atribui(b, num(6)), atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) } { ( ( ( a + 6 ) + ( a + 6 ) ) = 22 ) } [atribui(b, num(6))] { ( ( ( a + b ) + ( a + b ) ) = 22 ) } { ( ( ( a + b ) + ( a + b ) ) = 22 ) } [atribui(c, expInt(soma, ide(a), ide(b)))] { ( ( ( a + b ) + c ) = 22 ) }

Sentenças a serem provadas:

( true => ( ( ( 5 + 6 ) + ( 5 + 6 ) ) = 22 ) )