let X be StackAlgebra; for s being stack of X st not emp s holds
core (pop s) = core s
let s be stack of X; ( not emp s implies core (pop s) = core s )
set R = ConstructionRed X;
set A = the carrier' of X;
assume A1:
not emp s
; core (pop s) = core s
A2:
emp core (pop s)
by Def19;
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A3:
( t . 1 = pop s & t . (len t) = core (pop s) )
and
A4:
for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) )
by Def19;
[s,(pop s)] in ConstructionRed X
by A1, Def18;
then reconsider u = <*s,(pop s)*> as RedSequence of ConstructionRed X by REWRITE1:7;
( u . 2 = pop s & len u = 2 )
by FINSEQ_1:44;
then reconsider v = u $^ t as RedSequence of ConstructionRed X by A3, REWRITE1:8;
A5:
v = <*s*> ^ t
by REWRITE1:2;
then A6:
v . 1 = s
by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
A7:
len <*s*> = 1
by FINSEQ_1:40;
then A8:
len v = 1 + (len t)
by A5, FINSEQ_1:22;
len t in dom t
by FINSEQ_5:6;
then A9:
v . (len v) = t . (len t)
by A5, A7, A8, FINSEQ_1:def 7;
now for i being Nat st 1 <= i & i < len v holds
( not emp v /. i & v /. (i + 1) = pop (v /. i) )let i be
Nat;
( 1 <= i & i < len v implies ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) ) )assume A10:
( 1
<= i &
i < len v )
;
( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
(
i in dom v &
i + 1
in dom v )
by A10, MSUALG_8:1;
then A11:
(
v /. i = v . i &
v /. (i + 1) = v . (i + 1) )
by PARTFUN1:def 6;
consider j being
Nat such that A12:
i = 1
+ j
by A10, NAT_1:10;
A13:
j < len t
by A8, A10, A12, XREAL_1:6;
per cases
( i = 1 or i > 1 )
by A10, XXREAL_0:1;
suppose A14:
i = 1
;
( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )hence
not
emp v /. i
by A1, A5, A11, FINSEQ_1:41;
v /. (i + 1) = pop (v /. i)
1
in dom t
by FINSEQ_5:6;
hence v /. (i + 1) =
t . 1
by A5, A7, A11, A14, FINSEQ_1:def 7
.=
pop (v /. i)
by A14, A3, A5, A11, FINSEQ_1:41
;
verum end; suppose
i > 1
;
( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )then A15:
(
j >= 1 &
j in NAT )
by A12, NAT_1:13, ORDINAL1:def 12;
then
(
j in dom t &
i in dom t )
by A12, A13, MSUALG_8:1;
then
(
t . j = v . i &
t /. j = t . j &
t . i = v . (i + 1) &
t /. i = t . i )
by A5, A7, A12, FINSEQ_1:def 7, PARTFUN1:def 6;
hence
( not
emp v /. i &
v /. (i + 1) = pop (v /. i) )
by A4, A11, A12, A13, A15;
verum end; end;
hence
core (pop s) = core s
by A2, A3, A6, A9, Def19; verum