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