-- PUSHCOMPproof


Derivation of

s ~ s' ==> push(x,s) ~ push(x,s')

Applying the axiom resp. theorem

s ~ s' ===> top(s) = top(s') & pop(s) ~ pop(s')

at position [1] of the preceding formula leads to 

(s ~ s' ==> top(push(x,s)) = top(push(x,s'))) & 
(s ~ s' ==> pop(push(x,s)) ~ pop(push(x,s')))

The reducts have been simplified.

Applying the axiom resp. theorem

top(push(x,s)) = entry(x)

at position [0,1,0] of the preceding formula leads to 

(s ~ s' ==> entry(x) = top(push(x,s'))) & 
(s ~ s' ==> pop(push(x,s)) ~ pop(push(x,s')))

The reducts have been simplified.

Applying the axiom resp. theorem

top(push(x,s)) = entry(x)

at position [0,1,1] of the preceding formula leads to 

s ~ s' ==> pop(push(x,s)) ~ pop(push(x,s'))

The reducts have been simplified.

A transitivity axiom at position [1] of the preceding formula leads to 

s ~ s' ==> Any z0:(pop(push(x,s)) ~ z0 & z0 ~ pop(push(x,s')))

Applying the theorem

pop(push(x,s)) ~ s

at position [1,0,0] of the preceding formula leads to 

s ~ s' ==> s ~ pop(push(x,s'))

The reducts have been simplified.

A transitivity axiom at position [1] of the preceding formula leads to 

s ~ s' ==> Any z1:(s ~ z1 & z1 ~ pop(push(x,s')))

Applying the theorem

pop(push(x,s)) ~ s

at position [1,0,1] of the preceding formula leads to 

True

The reducts have been simplified.

Number of proof steps: 7

Solutions:

True