set R = ConstructionRed X;
deffunc H1( stack of X) -> stack of X = pop $1;
defpred S1[ set , stack of X, set ] means $3 = IFIN ($2, the s_empty of X,s,(pop $2));
A1:
for n being Nat
for x being stack of X ex y being stack of X st S1[n,x,y]
;
consider f being sequence of the carrier' of X such that
A2:
( f . 0 = s & ( for i being Nat holds S1[i,f . i,f . (i + 1)] ) )
from RECDEF_1:sch 2(A1);
defpred S2[ Nat] means ex s1 being stack of X st
( f . $1 = s1 & ( not emp s1 implies f . ($1 + 1) <> pop s1 ) );
A3:
ex i being Nat st S2[i]
by Def8;
consider i being Nat such that
A4:
( S2[i] & ( for j being Nat st S2[j] holds
i <= j ) )
from NAT_1:sch 5(A3);
deffunc H2( Nat) -> Element of the carrier' of X = f . ($1 -' 1);
consider t being FinSequence such that
A5:
( len t = i + 1 & ( for j being Nat st j in dom t holds
t . j = H2(j) ) )
from FINSEQ_1:sch 2();
consider s1 being stack of X such that
A6:
( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) )
by A4;
take
s1
; ( emp s1 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = s1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) )
f . (i + 1) = IFIN ((f . i), the s_empty of X,s,(pop (f . i)))
by A2;
then
( ( f . i in the s_empty of X implies f . (i + 1) = s ) & ( f . i nin the s_empty of X implies f . (i + 1) = pop (f . i) ) )
by MATRIX_7:def 1;
hence
emp s1
by A6; ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = s1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) )
A7:
t is RedSequence of ConstructionRed X
proof
thus
len t > 0
by A5;
REWRITE1:def 2 for b1 being set holds
( not b1 in dom t or not b1 + 1 in dom t or [(t . b1),(t . (b1 + 1))] in ConstructionRed X )
let j be
Nat;
( not j in dom t or not j + 1 in dom t or [(t . j),(t . (j + 1))] in ConstructionRed X )
assume A8:
(
j in dom t &
j + 1
in dom t )
;
[(t . j),(t . (j + 1))] in ConstructionRed X
then
(
j >= 1 &
j <= i + 1 &
j + 1
<= i + 1 )
by A5, FINSEQ_3:25;
then A9:
(
(j -' 1) + 1
= j &
(j + 1) -' 1
= j &
j <= i )
by NAT_D:34, XREAL_1:6, XREAL_1:235;
j -' 1
< i
by A9, NAT_1:13;
then A10:
not
emp f . (j -' 1)
by A4;
then A11:
f . (j -' 1) nin the
s_empty of
X
;
A12:
(
t . j = f . (j -' 1) &
t . (j + 1) = f . j )
by A5, A8, A9;
then
S1[
j -' 1,
f . (j -' 1),
t . (j + 1)]
by A2, A9;
then
t . (j + 1) = pop (f . (j -' 1))
by A11, MATRIX_7:def 1;
hence
[(t . j),(t . (j + 1))] in ConstructionRed X
by A12, A10, Def18;
verum
end;
then
1 in dom t
by FINSEQ_5:6;
then A13: t . 1 =
f . (1 -' 1)
by A5
.=
s
by A2, XREAL_1:232
;
then reconsider t = t as the carrier' of X -valued RedSequence of ConstructionRed X by A7, Th23;
take
t
; ( t . 1 = s & t . (len t) = s1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) )
thus
t . 1 = s
by A13; ( t . (len t) = s1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) )
len t in dom t
by FINSEQ_5:6;
hence t . (len t) =
f . ((i + 1) -' 1)
by A5
.=
s1
by A6, NAT_D:34
;
for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) )
let k be Nat; ( 1 <= k & k < len t implies ( not emp t /. k & t /. (k + 1) = pop (t /. k) ) )
assume A14:
( 1 <= k & k < len t )
; ( not emp t /. k & t /. (k + 1) = pop (t /. k) )
then
k in dom t
by FINSEQ_3:25;
then A15:
( t . k = f . (k -' 1) & t . k = t /. k )
by A5, PARTFUN1:def 6;
( 1 <= k + 1 & k + 1 <= len t )
by A14, NAT_1:13;
then
k + 1 in dom t
by FINSEQ_3:25;
then A16:
( t . (k + 1) = f . ((k + 1) -' 1) & t . (k + 1) = t /. (k + 1) )
by A5, PARTFUN1:def 6;
A17:
( (k -' 1) + 1 = k & (k + 1) -' 1 = k )
by A14, NAT_D:34, XREAL_1:235;
then
k -' 1 < i
by A5, A14, XREAL_1:6;
hence
not emp t /. k
by A4, A15; t /. (k + 1) = pop (t /. k)
then A18:
t /. k nin the s_empty of X
;
f . k = IFIN ((f . (k -' 1)), the s_empty of X,s,(pop (f . (k -' 1))))
by A2, A17;
hence
t /. (k + 1) = pop (t /. k)
by A15, A16, A17, A18, MATRIX_7:def 1; verum