-- TOPPUSHproof


Derivation of

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

Narrowing the preceding formula leads to 

Any f i:(top((upd(suc(i),x,f),suc(i))) = just(x) & s = (f,i))

Narrowing the preceding formula leads to 

Any f i:(top((upd(suc(i),x,f),suc(i))) = entry(x) & s = (f,i))

Simplifying the preceding formula leads to 

Any f i:(top(upd(suc(i),x,f),suc(i)) = entry(x) & s = (f,i))

Narrowing the preceding formula leads to 

Any f i:(get(upd(suc(i),x,f),suc(i)) = entry(x) & s = (f,i))

Narrowing the preceding formula leads to 

Any f i:((entry(x) = entry(x) | get(f,suc(i)) = entry(x) & suc(i) =/= suc(i)) & 
         s = (f,i))

Simplifying the preceding formula (7 steps) leads to 

Any f i:(s = (f,i))

Applying the theorem

True ===> Any f i:(s = (f,i))

at position [] of the preceding formula leads to 

All s0:(Any f2 i2:(s0 = (f2,i2))) ==> Any f i:(s = (f,i))

Simplifying the preceding formula leads to 

True

Number of proof steps: 8

Solutions:

True