set X = StandardStackSystem A;
let f be sequence of the carrier' of (StandardStackSystem A); STACKS_1:def 8 ex i being Nat ex s being stack of (StandardStackSystem A) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
assume A1:
for i being Nat
for s being stack of (StandardStackSystem A) st f . i = s holds
( not emp s & f . (i + 1) = pop s )
; contradiction
reconsider g = f . 1 as Element of A * by Def7;
defpred S1[ Nat] means ex i being Nat ex g being Element of A * st
( g = f . i & A = len g );
A2:
ex k being Nat st S1[k]
proof
take k =
len g;
S1[k]
take i = 1;
ex g being Element of A * st
( g = f . i & k = len g )
take
g
;
( g = f . i & k = len g )
thus
(
g = f . i &
k = len g )
;
verum
end;
A3:
for k being Nat st k <> 0 & S1[k] holds
ex n being Nat st
( n < k & S1[n] )
proof
let k be
Nat;
( k <> 0 & S1[k] implies ex n being Nat st
( n < k & S1[n] ) )
assume A4:
k <> 0
;
( not S1[k] or ex n being Nat st
( n < k & S1[n] ) )
then consider n0 being
Nat such that A5:
k = n0 + 1
by NAT_1:6;
given i being
Nat,
g being
Element of
A * such that A6:
(
g = f . i &
k = len g )
;
ex n being Nat st
( n < k & S1[n] )
reconsider s =
g as
stack of
(StandardStackSystem A) by A6;
reconsider h =
pop s as
Element of
A * by Def7;
take n =
len h;
( n < k & S1[n] )
A7:
not
s is
empty
by A4, A6;
then
not
emp s
by Def7;
then A8:
(
f . (i + 1) = pop s &
h = Del (
g,1) )
by A1, A6, Def7;
1
in dom g
by A7, FINSEQ_5:6;
then
n0 = n
by A5, A6, A8, FINSEQ_3:109;
hence
(
n < k &
S1[
n] )
by A5, A8, NAT_1:13;
verum
end;
S1[ 0 ]
from NAT_1:sch 7(A2, A3);
then consider i being Nat, g being Element of A * such that
A9:
( g = f . i & 0 = len g )
;
reconsider s = g as stack of (StandardStackSystem A) by A9;
( g is empty & not emp s )
by A1, A9;
hence
contradiction
by Def7; verum