Prova:

{ ( 5 = 5 ) } [atribui(A, num(5))] { ( 5 = 5 ) }

Prova:

{ ( 5 = 5 ) } [atribui(A, num(5))] { ( 5 = 5 ) } { ( 5 = 5 ) } [atribui(A, num(5))] { ( 5 = A ) } ( ( 5 = A ) => ( 5 = 5 ) )

Sentenças a serem provadas:

( ( 5 = A ) => ( 5 = 5 ) )

Prova:

{ ( 5 = 5 ) } [atribui(A, num(5))] { ( 5 = 5 ) } { ( 5 = 5 ) } [atribui(A, num(5))] { ( A = 5 ) } ( ( A = 5 ) => ( 5 = 5 ) )

Sentenças a serem provadas:

( ( A = 5 ) => ( 5 = 5 ) )

Prova:

{ ( 5 = 5 ) } [atribui(A, num(5))] { ( 5 = 5 ) } { ( 5 = 5 ) } [atribui(A, num(5))] { ( A = A ) } ( ( A = A ) => ( 5 = 5 ) )

Sentenças a serem provadas:

( ( A = A ) => ( 5 = 5 ) )