let X be non empty non void StackSystem ; :: thesis: 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; :: thesis: 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; :: thesis: ( X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) implies ( e1 = e2 & s1 = s2 ) )
assume X is top-push ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum