:: deftheorem Def19 defines core STACKS_1:def 19 :
for X being StackAlgebra
for s, b₃ being stack of X holds
( b₃ = core s iff ( emp b₃ & ex t being the carrier' of b₁ -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b₃ & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) ) );