let X be non empty non void StackSystem ; :: thesis: for s1, s2 being stack of X st X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 holds
s1 = s2
let s1, s2 be stack of X; :: thesis: ( X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 implies s1 = s2 )
assume A1: X is push-pop ; :: thesis: ( emp s1 or emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 )
assume not emp s1 ; :: thesis: ( emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 )
then s1 = push ((top s1),(pop s1)) by A1;
hence ( emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 ) by A1; :: thesis: verum