-- POPEMPTYproof


Derivation of

pop(empty) ~ empty

Applying the axiom resp. theorem

empty = (new,0)

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

pop((new,0)) ~ (new,0)

Simplifying the preceding formula leads to 

pop(new,0) ~ (new,0)

Applying the axiom resp. theorem

pop(f,i) = (f,pred(i))

at position [0] of the preceding formula leads to 

(new,pred(0)) ~ (new,0)

Applying the axiom resp. theorem

pred(0) = 0

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

(new,0) ~ (new,0)

Simplifying the preceding formula leads to 

True

Number of proof steps: 5

Solutions:

True