Prova:

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

Sentenças a serem provadas:

( ( 5 = 5 ) => ( a = 5 ) )

Prova:

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

Sentenças a serem provadas:

( ( 5 = a ) => ( a = 5 ) )

Prova:

{ ( 5 = 5 ) } [atribui(a, num(5)), skip] { ( a = 5 ) } { ( 5 = 5 ) } [atribui(a, num(5))] { ( a = 5 ) } { ( a = 5 ) } [skip] { ( a = 5 ) }

Prova:

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

Sentenças a serem provadas:

( ( a = a ) => ( a = 5 ) )