:: deftheorem Def7 defines StandardStackSystem STACKS_1:def 7 :
for A being non empty set
for b₂ being non empty non void strict StackSystem holds
( b₂ = StandardStackSystem A iff ( the carrier of b₂ = A & the carrier' of b₂ = A * & ( for s being stack of b₂ holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of b₂ & pop s = {} ) ) & ( for e being Element of b₂ holds push (e,s) = <*e*> ^ g ) ) ) ) ) ) );