:: STACKS_1 semantic presentation

begin


definition
let A be set ;
let s1, s2 be FinSequence of A;
:: original: ^
redefine funcs1 ^ s2 ->  Element of A * ;
coherence
 s1 ^ s2 is Element of A *
proof
 s1 ^ s2 is FinSequence of A ;
hence  s1 ^ s2 is Element of A * by FINSEQ_1:def_11; ::_thesis: verum
end;
end;

definition
let A be set ;
let i be Nat;
let s be FinSequence of A;
:: original: Del
redefine func Del (s,i) ->  Element of A * ;
coherence
 Del (s,i) is Element of A *
proof
 ( rng (Del (s,i)) c= rng s & rng s c= A ) by FINSEQ_3:106;
then  rng (Del (s,i)) c= A by XBOOLE_1:1;
then  Del (s,i) is FinSequence of A by FINSEQ_1:def_4;
hence  Del (s,i) is Element of A * by FINSEQ_1:def_11; ::_thesis: verum
end;
end;

theorem Th1: :: STACKS_1:1
for i being Nat holds Del ({},i) = {}
proof
let i be Nat; ::_thesis: Del ({},i) = {}
 dom (Del ({},i)) c= dom {} by WSIERP_1:39;
hence  Del ({},i) = {} ; ::_thesis: verum
end;

scheme :: STACKS_1:sch 1
IndSeqD{ F1() ->  non empty set , P1[ set ] } :
 for p being FinSequence of F1() holds P1[p]
provided
A1: P1[ <*> F1()] and
A2: for p being FinSequence of F1()
for x being Element of F1() st P1[p] holds
P1[<*x*> ^ p]
proof
defpred S1[ set ] means  for p being FinSequence of F1() st len p = $1 holds
P1[p];
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: for p being FinSequence of F1() st len p = i holds
P1[p] ; ::_thesis: S1[i + 1]
let p be FinSequence of F1(); ::_thesis: ( len p = i + 1 implies P1[p] )
assume A5: len p = i + 1 ; ::_thesis: P1[p]
then  p <> {} ;
then consider q being FinSequence of F1(), x being Element of F1() such that
A6: p = <*x*> ^ q by FINSEQ_2:130;
 len p = (len q) + 1 by A6, FINSEQ_5:8;
hence  P1[p] by A2, A4, A5, A6; ::_thesis: verum
end;
let p be FinSequence of F1(); ::_thesis: P1[p]
A7: len p = len p ;
A8: S1[ 0 ]
proof
let p be FinSequence of F1(); ::_thesis: ( len p = 0 implies P1[p] )
assume  len p = 0 ; ::_thesis: P1[p]
then  p = <*> F1() ;
hence  P1[p] by A1; ::_thesis: verum
end;
 for i being Nat holds S1[i] from NAT_1:sch_2(A8, A3);
hence  P1[p] by A7; ::_thesis: verum
end;

definition
let C, D be non empty set ;
let R be Relation;
mode BinOp of C,D,R ->  Function of [:C,D:],D means :Def1: :: STACKS_1:def 1
 for x being Element of C
for y1, y2 being Element of D st [y1,y2] in R holds
[(it . (x,y1)),(it . (x,y2))] in R;
existence
 ex b1 being Function of [:C,D:],D st
for x being Element of C
for y1, y2 being Element of D st [y1,y2] in R holds
[(b1 . (x,y1)),(b1 . (x,y2))] in R
proof
take f = pr2 (C,D); ::_thesis: for x being Element of C
for y1, y2 being Element of D st [y1,y2] in R holds
[(f . (x,y1)),(f . (x,y2))] in R
let x be Element of C; ::_thesis: for y1, y2 being Element of D st [y1,y2] in R holds
[(f . (x,y1)),(f . (x,y2))] in R
let y1, y2 be Element of D; ::_thesis: ( [y1,y2] in R implies [(f . (x,y1)),(f . (x,y2))] in R )
 f . (x,y1) = y1 by FUNCT_3:def_5;
hence  ( [y1,y2] in R implies [(f . (x,y1)),(f . (x,y2))] in R ) by FUNCT_3:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines BinOp STACKS_1:def_1_:_
 for C, D being non empty set
for R being Relation
for b4 being Function of [:C,D:],D holds
( b4 is BinOp of C,D,R iff for x being Element of C
for y1, y2 being Element of D st [y1,y2] in R holds
[(b4 . (x,y1)),(b4 . (x,y2))] in R );

scheme :: STACKS_1:sch 2
LambdaD2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F3() } :
 ex M being Function of [:F1(),F2():],F3() st
for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j)
proof
consider M being ManySortedSet of [:F1(),F2():] such that
A1: for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j) from ALTCAT_1:sch_2();
A2: dom M = [:F1(),F2():] by PARTFUN1:def_2;
 rng M c= F3()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng M or y in F3() )
assume  y in rng M ; ::_thesis: y in F3()
then consider x being set  such that
A3: ( x in dom M & y = M . x ) by FUNCT_1:def_3;
consider x1, x2 being set  such that
A4: ( x1 in F1() & x2 in F2() & x = [x1,x2] ) by A3, ZFMISC_1:def_2;
y = M . (x1,x2) by A3, A4
.= F4(x1,x2) by A1, A4 ;
hence  y in F3() ; ::_thesis: verum
end;
then reconsider M = M as Function of [:F1(),F2():],F3() by A2, FUNCT_2:2;
take  M ; ::_thesis: for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j)
thus  for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F4(i,j) by A1; ::_thesis: verum
end;

definition
let C, D be non empty set ;
let R be Equivalence_Relation of D;
let b be Function of [:C,D:],D;
assume A1: b is BinOp of C,D,R ;
funcb /\/ R ->  Function of [:C,(Class R):],(Class R) means :Def2: :: STACKS_1:def 2
 for x, y, y1 being set st x in C & y in Class R & y1 in y holds
it . (x,y) = Class (R,(b . (x,y1)));
existence
 ex b1 being Function of [:C,(Class R):],(Class R) st
for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1)))
proof
now__::_thesis:_for_X_being_set_st_X_in_Class_R_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in Class R implies X <> {} )
assume  X in Class R ; ::_thesis: X <> {}
then  ex x being set st
( x in D & X = Class (R,x) ) by EQREL_1:def_3;
hence  X <> {} by EQREL_1:20; ::_thesis: verum
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X being set st X in Class R holds
g . X in X by FUNCT_1:111;
A4: rng g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in D )
assume  x in rng g ; ::_thesis: x in D
then consider y being set  such that
A5: y in dom g and
A6: x = g . y by FUNCT_1:def_3;
 x in y by A2, A3, A5, A6;
hence  x in D by A2, A5; ::_thesis: verum
end;
deffunc H1( Element of D) ->  Element of Class R = EqClass (R,$1);
consider f being Function of D,(Class R) such that
A7: for x being Element of D holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider g = g as Function of (Class R),D by A2, A4, FUNCT_2:def_1, RELSET_1:4;
deffunc H2( Element of C, Element of Class R) ->  Element of Class R = f . (b . ($1,(g . $2)));
consider bR being Function of [:C,(Class R):],(Class R) such that
A8: for x being Element of C
for y being Element of Class R holds bR . (x,y) = H2(x,y) from STACKS_1:sch_2();
take  bR ; ::_thesis: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
bR . (x,y) = Class (R,(b . (x,y1)))
let x, y, y1 be set ; ::_thesis: ( x in C & y in Class R & y1 in y implies bR . (x,y) = Class (R,(b . (x,y1))) )
assume that
A9: x in C and
A10: y in Class R and
A11: y1 in y ; ::_thesis: bR . (x,y) = Class (R,(b . (x,y1)))
reconsider x9 = x as Element of C by A9;
reconsider y9 = y as Element of Class R by A10;
reconsider y19 = y1 as Element of D by A10, A11;
A12: ex y2 being set st
( y2 in D & y9 = Class (R,y2) ) by EQREL_1:def_3;
 g . y9 in y by A3;
then  [(g . y9),y19] in R by A11, A12, EQREL_1:22;
then  [(b . (x9,(g . y9))),(b . (x9,y19))] in R by A1, Def1;
then A13: b . (x9,(g . y9)) in EqClass (R,(b . (x9,y19))) by EQREL_1:19;
A14: f . (b . (x9,(g . y9))) = EqClass (R,(b . (x9,(g . y9)))) by A7;
 bR . (x9,y9) = f . (b . (x9,(g . y9))) by A8;
hence  bR . (x,y) = Class (R,(b . (x,y1))) by A13, A14, EQREL_1:23; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:C,(Class R):],(Class R) st ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) ) & ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ) holds
b1 = b2
proof
let b1, b2 be Function of [:C,(Class R):],(Class R); ::_thesis: ( ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) ) & ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ) implies b1 = b2 )
assume that
A15: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) and
A16: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ; ::_thesis: b1 = b2
now__::_thesis:_for_x_being_Element_of_C
for_y_being_Element_of_Class_R_holds_b1_._(x,y)_=_b2_._(x,y)
let x be Element of C; ::_thesis: for y being Element of Class R holds b1 . (x,y) = b2 . (x,y)
let y be Element of Class R; ::_thesis: b1 . (x,y) = b2 . (x,y)
consider y1 being set  such that
A17: y1 in D and
A18: y = Class (R,y1) by EQREL_1:def_3;
 b1 . (x,y) = Class (R,(b . (x,y1))) by A15, A17, A18, EQREL_1:20;
hence  b1 . (x,y) = b2 . (x,y) by A16, A17, A18, EQREL_1:20; ::_thesis: verum
end;
hence  b1 = b2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines /\/ STACKS_1:def_2_:_
 for C, D being non empty set
for R being Equivalence_Relation of D
for b being Function of [:C,D:],D st b is BinOp of C,D,R holds
for b5 being Function of [:C,(Class R):],(Class R) holds
( b5 = b /\/ R iff for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b5 . (x,y) = Class (R,(b . (x,y1))) );

definition
let A, B be non empty set ;
let C be Subset of A;
let D be Subset of B;
let f be Function of A,B;
let g be Function of C,D;
:: original: +*
redefine funcf +* g ->  Function of A,B;
coherence
 f +* g is Function of A,B
proof
percases ( D = {} or D <> {} ) ;
suppose D = {} ; ::_thesis: f +* g is Function of A,B
then A1: g = {} ;
 f +* {} = f ;
hence  f +* g is Function of A,B by A1; ::_thesis: verum
end;
supposeA2: D <> {} ; ::_thesis: f +* g is Function of A,B
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1
.= A \/ (dom g) by FUNCT_2:def_1
.= A \/ C by A2, FUNCT_2:def_1
.= A by XBOOLE_1:12 ;
A4: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
 ( (rng f) \/ (rng g) c= B \/ D & B \/ D = B ) by XBOOLE_1:12, XBOOLE_1:13;
hence  f +* g is Function of A,B by A3, A4, FUNCT_2:2, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
end;

begin

definition
attrc1 is strict ;
struct StackSystem  ->  2-sorted ;
aggrStackSystem(# carrier, carrier', s_empty, s_push, s_pop, s_top #) ->  StackSystem ;
sel s_empty c1 ->  Subset of the carrier' of c1;
sel s_push c1 ->  Function of [: the carrier of c1, the carrier' of c1:], the carrier' of c1;
sel s_pop c1 ->  Function of the carrier' of c1, the carrier' of c1;
sel s_top c1 ->  Function of the carrier' of c1, the carrier of c1;
end;

registration
let a1 be non empty set ;
let a2 be set ;
let a3 be Subset of a2;
let a4 be Function of [:a1,a2:],a2;
let a5 be Function of a2,a2;
let a6 be Function of a2,a1;
cluster StackSystem(# a1,a2,a3,a4,a5,a6 #) ->  non empty ;
coherence
 not StackSystem(# a1,a2,a3,a4,a5,a6 #) is empty ;
end;

registration
let a1 be set ;
let a2 be non empty set ;
let a3 be Subset of a2;
let a4 be Function of [:a1,a2:],a2;
let a5 be Function of a2,a2;
let a6 be Function of a2,a1;
cluster StackSystem(# a1,a2,a3,a4,a5,a6 #) ->  non void ;
coherence
 not StackSystem(# a1,a2,a3,a4,a5,a6 #) is void ;
end;

registration
cluster non empty non void strict for StackSystem ;
existence
 ex b1 being StackSystem st
( not b1 is empty & not b1 is void & b1 is strict )
proof
set a1 = the non empty set ;
set a2 = the non empty set ;
set a3 = the Subset of the non empty set ;
set a4 = the Function of [: the non empty set , the non empty set :], the non empty set ;
set a5 = the Function of the non empty set , the non empty set ;
set a6 = the Function of the non empty set , the non empty set ;
take  StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) ; ::_thesis: ( not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is empty & not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is void & StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is strict )
thus  ( not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is empty & not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is void & StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is strict ) ; ::_thesis: verum
end;
end;

definition
let X be StackSystem ;
mode stack of X is Element of the carrier' of X;
end;

definition
let X be StackSystem ;
let s be stack of X;
pred emp s means :Def3: :: STACKS_1:def 3
s in the s_empty of X;
end;

:: deftheorem Def3 defines emp STACKS_1:def_3_:_
 for X being StackSystem
for s being stack of X holds
( emp s iff s in the s_empty of X );

definition
let X be non void StackSystem ;
let s be stack of X;
func pop s ->  stack of X equals :: STACKS_1:def 4
 the s_pop of X . s;
coherence
 the s_pop of X . s is stack of X ;
func top s ->  Element of X equals :: STACKS_1:def 5
 the s_top of X . s;
coherence
 the s_top of X . s is Element of X ;
end;

:: deftheorem  defines pop STACKS_1:def_4_:_
 for X being non void StackSystem
for s being stack of X holds pop s = the s_pop of X . s;

:: deftheorem  defines top STACKS_1:def_5_:_
 for X being non void StackSystem
for s being stack of X holds top s = the s_top of X . s;

definition
let X be non empty non void StackSystem ;
let s be stack of X;
let e be Element of X;
func push (e,s) ->  stack of X equals :: STACKS_1:def 6
 the s_push of X . (e,s);
coherence
 the s_push of X . (e,s) is stack of X ;
end;

:: deftheorem  defines push STACKS_1:def_6_:_
 for X being non empty non void StackSystem
for s being stack of X
for e being Element of X holds push (e,s) = the s_push of X . (e,s);

definition
let A be non empty set ;
func StandardStackSystem A ->  non empty non void strict StackSystem  means :Def7: :: STACKS_1:def 7
( the carrier of it = A & the carrier' of it = A * & ( for s being stack of it 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 it & pop s = {} ) ) & ( for e being Element of it holds push (e,s) = <*e*> ^ g ) ) ) ) ) );
existence
 ex b1 being non empty non void strict StackSystem st
( the carrier of b1 = A & the carrier' of b1 = A * & ( for s being stack of b1 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 b1 & pop s = {} ) ) & ( for e being Element of b1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) )
proof
reconsider s0 = <*> A as Element of A * by FINSEQ_1:def_11;
set E = {s0};
deffunc H1( Element of A, Element of A * ) ->  Element of A * = <*$1*> ^ $2;
deffunc H2( Element of A * ) ->  Element of A * = Del ($1,1);
deffunc H3( Element of A * ) ->  Element of A = IFEQ ($1,{}, the Element of A,($1 /. 1));
consider psh being Function of [:A,(A *):],(A *) such that
A1: for a being Element of A
for s being Element of A * holds psh . (a,s) = H1(a,s) from BINOP_1:sch_4();
consider pp being Function of (A *),(A *) such that
A2: for s being Element of A * holds pp . s = H2(s) from FUNCT_2:sch_4();
consider tp being Function of (A *),A such that
A3: for s being Element of A * holds tp . s = H3(s) from FUNCT_2:sch_4();
take X = StackSystem(# A,(A *),{s0},psh,pp,tp #); ::_thesis: ( the carrier of X = A & the carrier' of X = A * & ( for s being stack of X 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) ) ) )
thus  ( the carrier of X = A & the carrier' of X = A * ) ; ::_thesis: for s being stack of X 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
let s be stack of X; ::_thesis: ( ( 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
 ( emp s iff s in {s0} ) by Def3;
hence A4: ( emp s iff s is empty ) by TARSKI:def_1; ::_thesis: 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
let g be FinSequence; ::_thesis: ( g = s implies ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) )
assume A5: g = s ; ::_thesis: ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
then reconsider h = g as Element of A * ;
hereby  ::_thesis: ( ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
assume A6: not emp s ; ::_thesis: ( top s = g . 1 & pop s = Del (g,1) )
then A7: 1 in dom h by A4, A5, FINSEQ_5:6;
thus  top s = IFEQ (s,{}, the Element of A,(h /. 1)) by A3, A5
.= h /. 1 by A4, A6, FUNCOP_1:def_8
.= g . 1 by A7, PARTFUN1:def_6 ; ::_thesis: pop s = Del (g,1)
thus  pop s = Del (g,1) by A5, A2; ::_thesis: verum
end;
hereby  ::_thesis: for e being Element of X holds push (e,s) = <*e*> ^ g
assume A8: emp s ; ::_thesis: ( top s = the Element of X & pop s = {} )
thus  top s = IFEQ (s,{}, the Element of A,(h /. 1)) by A3, A5
.= the Element of X by A4, A8, FUNCOP_1:def_8 ; ::_thesis: pop s = {}
thus  pop s = Del (g,1) by A5, A2
.= {} by A4, A5, A8, Th1 ; ::_thesis: verum
end;
let e be Element of X; ::_thesis: push (e,s) = <*e*> ^ g
thus  push (e,s) = <*e*> ^ g by A1, A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty non void strict StackSystem st the carrier of b1 = A & the carrier' of b1 = A * & ( for s being stack of b1 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 b1 & pop s = {} ) ) & ( for e being Element of b1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) & the carrier of b2 = A & the carrier' of b2 = A * & ( for s being stack of b2 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 b2 & pop s = {} ) ) & ( for e being Element of b2 holds push (e,s) = <*e*> ^ g ) ) ) ) ) holds
b1 = b2
proof
let X1, X2 be non empty non void strict StackSystem ; ::_thesis: ( the carrier of X1 = A & the carrier' of X1 = A * & ( for s being stack of X1 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 X1 & pop s = {} ) ) & ( for e being Element of X1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) & the carrier of X2 = A & the carrier' of X2 = A * & ( for s being stack of X2 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 X2 & pop s = {} ) ) & ( for e being Element of X2 holds push (e,s) = <*e*> ^ g ) ) ) ) ) implies X1 = X2 )
assume that
A9: the carrier of X1 = A and
A10: the carrier' of X1 = A * and
A11: for s being stack of X1 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 X1 & pop s = {} ) ) & ( for e being Element of X1 holds push (e,s) = <*e*> ^ g ) ) ) ) and
A12: the carrier of X2 = A and
A13: the carrier' of X2 = A * and
A14: for s being stack of X2 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 X2 & pop s = {} ) ) & ( for e being Element of X2 holds push (e,s) = <*e*> ^ g ) ) ) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_Element_of_A
for_y_being_Element_of_A_*_holds_the_s_push_of_X1_._(x,y)_=_the_s_push_of_X2_._(x,y)
let x be Element of A; ::_thesis: for y being Element of A * holds the s_push of X1 . (x,y) = the s_push of X2 . (x,y)
reconsider e1 = x as Element of X1 by A9;
reconsider e2 = x as Element of X2 by A12;
let y be Element of A * ; ::_thesis: the s_push of X1 . (x,y) = the s_push of X2 . (x,y)
reconsider s1 = y as stack of X1 by A10;
reconsider s2 = y as stack of X2 by A13;
thus  the s_push of X1 . (x,y) = push (e1,s1)
.= <*x*> ^ y by A11
.= push (e2,s2) by A14
.= the s_push of X2 . (x,y) ; ::_thesis: verum
end;
then A15: the s_push of X1 = the s_push of X2 by A9, A10, A12, A13, BINOP_1:2;
now__::_thesis:_for_x_being_Element_of_A_*_holds_the_s_pop_of_X1_._x_=_the_s_pop_of_X2_._x
let x be Element of A * ; ::_thesis: the s_pop of X1 . b1 = the s_pop of X2 . b1
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;
percases ( not emp s1 or emp s1 ) ;
supposeA16: not emp s1 ; ::_thesis: the s_pop of X1 . b1 = the s_pop of X2 . b1
then  not s1 is empty by A11;
then A17: not emp s2 by A14;
thus  the s_pop of X1 . x = pop s1
.= Del (x,1) by A16, A11
.= pop s2 by A17, A14
.= the s_pop of X2 . x ; ::_thesis: verum
end;
supposeA18: emp s1 ; ::_thesis: the s_pop of X1 . b1 = the s_pop of X2 . b1
then  s1 is empty by A11;
then A19: emp s2 by A14;
thus  the s_pop of X1 . x = pop s1
.= {} by A18, A11
.= pop s2 by A19, A14
.= the s_pop of X2 . x ; ::_thesis: verum
end;
end;
end;
then A20: the s_pop of X1 = the s_pop of X2 by A10, A13, FUNCT_2:63;
A21: now__::_thesis:_for_x_being_Element_of_A_*_holds_the_s_top_of_X1_._x_=_the_s_top_of_X2_._x
let x be Element of A * ; ::_thesis: the s_top of X1 . b1 = the s_top of X2 . b1
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;
percases ( not emp s1 or emp s1 ) ;
supposeA22: not emp s1 ; ::_thesis: the s_top of X1 . b1 = the s_top of X2 . b1
then  not s1 is empty by A11;
then A23: not emp s2 by A14;
thus  the s_top of X1 . x = top s1
.= x . 1 by A22, A11
.= top s2 by A23, A14
.= the s_top of X2 . x ; ::_thesis: verum
end;
supposeA24: emp s1 ; ::_thesis: the s_top of X1 . b1 = the s_top of X2 . b1
then  s1 is empty by A11;
then A25: emp s2 by A14;
thus  the s_top of X1 . x = top s1
.= the Element of A by A9, A24, A11
.= top s2 by A12, A25, A14
.= the s_top of X2 . x ; ::_thesis: verum
end;
end;
end;
 the s_empty of X1 = the s_empty of X2
proof
thus  the s_empty of X1 c= the s_empty of X2 :: according to XBOOLE_0:def_10 ::_thesis: the s_empty of X2 c= the s_empty of X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the s_empty of X1 or x in the s_empty of X2 )
assume A26: x in the s_empty of X1 ; ::_thesis: x in the s_empty of X2
then reconsider s1 = x as stack of X1 ;
reconsider s2 = s1 as stack of X2 by A10, A13;
 emp s1 by A26, Def3;
then  s1 is empty by A11;
then  emp s2 by A14;
hence  x in the s_empty of X2 by Def3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the s_empty of X2 or x in the s_empty of X1 )
assume A27: x in the s_empty of X2 ; ::_thesis: x in the s_empty of X1
then reconsider s2 = x as stack of X2 ;
reconsider s1 = s2 as stack of X1 by A10, A13;
 emp s2 by A27, Def3;
then  s2 is empty by A14;
then  emp s1 by A11;
hence  x in the s_empty of X1 by Def3; ::_thesis: verum
end;
hence  X1 = X2 by A9, A10, A12, A13, A15, A20, A21, FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines StandardStackSystem STACKS_1:def_7_:_
 for A being non empty set
for b2 being non empty non void strict StackSystem holds
( b2 = StandardStackSystem A iff ( the carrier of b2 = A & the carrier' of b2 = A * & ( for s being stack of b2 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 b2 & pop s = {} ) ) & ( for e being Element of b2 holds push (e,s) = <*e*> ^ g ) ) ) ) ) ) );


registration
let A be non empty set ;
cluster the carrier' of (StandardStackSystem A) ->  functional ;
coherence
 the carrier' of (StandardStackSystem A) is functional
proof
 the carrier' of (StandardStackSystem A) = A * by Def7;
hence  the carrier' of (StandardStackSystem A) is functional ; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster  ->  FinSequence-like for Element of the carrier' of (StandardStackSystem A);
coherence
 for b1 being stack of (StandardStackSystem A) holds b1 is FinSequence-like
proof
 the carrier' of (StandardStackSystem A) = A * by Def7;
hence  for b1 being stack of (StandardStackSystem A) holds b1 is FinSequence-like ; ::_thesis: verum
end;
end;


definition
let X be non empty non void StackSystem ;
attrX is pop-finite  means :Def8: :: STACKS_1:def 8
 for f being Function of NAT, the carrier' of X ex i being Nat ex s being stack of X st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) );
attrX is push-pop  means :Def9: :: STACKS_1:def 9
 for s being stack of X st not emp s holds
s = push ((top s),(pop s));
attrX is top-push  means :Def10: :: STACKS_1:def 10
 for s being stack of X
for e being Element of X holds e = top (push (e,s));
attrX is pop-push  means :Def11: :: STACKS_1:def 11
 for s being stack of X
for e being Element of X holds s = pop (push (e,s));
attrX is push-non-empty  means :Def12: :: STACKS_1:def 12
 for s being stack of X
for e being Element of X holds not emp push (e,s);
end;

:: deftheorem Def8 defines pop-finite STACKS_1:def_8_:_
 for X being non empty non void StackSystem holds
( X is pop-finite iff for f being Function of NAT, the carrier' of X ex i being Nat ex s being stack of X st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) );

:: deftheorem Def9 defines push-pop STACKS_1:def_9_:_
 for X being non empty non void StackSystem holds
( X is push-pop iff for s being stack of X st not emp s holds
s = push ((top s),(pop s)) );

:: deftheorem Def10 defines top-push STACKS_1:def_10_:_
 for X being non empty non void StackSystem holds
( X is top-push iff for s being stack of X
for e being Element of X holds e = top (push (e,s)) );

:: deftheorem Def11 defines pop-push STACKS_1:def_11_:_
 for X being non empty non void StackSystem holds
( X is pop-push iff for s being stack of X
for e being Element of X holds s = pop (push (e,s)) );

:: deftheorem Def12 defines push-non-empty STACKS_1:def_12_:_
 for X being non empty non void StackSystem holds
( X is push-non-empty iff for s being stack of X
for e being Element of X holds not emp push (e,s) );

registration
let A be non empty set ;
cluster StandardStackSystem A ->  non empty non void strict pop-finite ;
coherence
 StandardStackSystem A is pop-finite
proof
set X = StandardStackSystem A;
let f be Function of NAT, the carrier' of (StandardStackSystem A); :: according to STACKS_1:def_8 ::_thesis: 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 ) ; ::_thesis: 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; ::_thesis: S1[k]
take i = 1; ::_thesis: ex g being Element of A * st
( g = f . i & k = len g )
take  g ; ::_thesis: ( g = f . i & k = len g )
thus  ( g = f . i & k = len g ) ; ::_thesis: 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; ::_thesis: ( k <> 0 & S1[k] implies ex n being Nat st
( n < k & S1[n] ) )
assume A4: k <> 0 ; ::_thesis: ( 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 ) ; ::_thesis: 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; ::_thesis: ( 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; ::_thesis: 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; ::_thesis: verum
end;
cluster StandardStackSystem A ->  non empty non void strict push-pop ;
coherence
 StandardStackSystem A is push-pop
proof
set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def_9 ::_thesis: ( not emp s implies s = push ((top s),(pop s)) )
reconsider g = s as Element of A * by Def7;
assume A10: not emp s ; ::_thesis: s = push ((top s),(pop s))
then A11: not s is empty by Def7;
then A12: g = <*(g . 1)*> ^ (Del (g,1)) by POLYALG1:4;
reconsider h = Del (g,1) as stack of (StandardStackSystem A) by Def7;
 1 in dom g by A11, FINSEQ_5:6;
then  g . 1 in A by FUNCT_1:102;
then reconsider x = g . 1 as Element of (StandardStackSystem A) by Def7;
thus s = push (x,h) by A12, Def7
.= push ((top s),h) by A10, Def7
.= push ((top s),(pop s)) by A10, Def7 ; ::_thesis: verum
end;
cluster StandardStackSystem A ->  non empty non void strict top-push ;
coherence
 StandardStackSystem A is top-push
proof
set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def_10 ::_thesis: for e being Element of (StandardStackSystem A) holds e = top (push (e,s))
let e be Element of (StandardStackSystem A); ::_thesis: e = top (push (e,s))
reconsider g = s as Element of A * by Def7;
reconsider h = push (e,s) as Element of A * by Def7;
A13: h = <*e*> ^ g by Def7;
then A14: not emp push (e,s) by Def7;
thus e = h . 1 by A13, FINSEQ_1:41
.= top (push (e,s)) by A14, Def7 ; ::_thesis: verum
end;
cluster StandardStackSystem A ->  non empty non void strict pop-push ;
coherence
 StandardStackSystem A is pop-push
proof
set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def_11 ::_thesis: for e being Element of (StandardStackSystem A) holds s = pop (push (e,s))
let e be Element of (StandardStackSystem A); ::_thesis: s = pop (push (e,s))
reconsider g = s as Element of A * by Def7;
reconsider h = push (e,s) as Element of A * by Def7;
A15: h = <*e*> ^ g by Def7;
then A16: not emp push (e,s) by Def7;
thus s = Del ((<*e*> ^ g),1) by WSIERP_1:40
.= pop (push (e,s)) by A15, A16, Def7 ; ::_thesis: verum
end;
cluster StandardStackSystem A ->  non empty non void strict push-non-empty ;
coherence
 StandardStackSystem A is push-non-empty
proof
set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def_12 ::_thesis: for e being Element of (StandardStackSystem A) holds not emp push (e,s)
let e be Element of (StandardStackSystem A); ::_thesis: not emp push (e,s)
reconsider g = s as Element of A * by Def7;
 push (e,s) = <*e*> ^ g by Def7;
hence  not emp push (e,s) by Def7; ::_thesis: verum
end;
end;

registration
cluster non empty non void V67() strict pop-finite push-pop top-push pop-push push-non-empty for StackSystem ;
existence
 ex b1 being non empty non void StackSystem st
( b1 is pop-finite & b1 is push-pop & b1 is top-push & b1 is pop-push & b1 is push-non-empty & b1 is strict )
proof
take  StandardStackSystem the non empty set ; ::_thesis: ( StandardStackSystem the non empty set is pop-finite & StandardStackSystem the non empty set is push-pop & StandardStackSystem the non empty set is top-push & StandardStackSystem the non empty set is pop-push & StandardStackSystem the non empty set is push-non-empty & StandardStackSystem the non empty set is strict )
thus  ( StandardStackSystem the non empty set is pop-finite & StandardStackSystem the non empty set is push-pop & StandardStackSystem the non empty set is top-push & StandardStackSystem the non empty set is pop-push & StandardStackSystem the non empty set is push-non-empty & StandardStackSystem the non empty set is strict ) ; ::_thesis: verum
end;
end;

definition
mode StackAlgebra is non empty non void pop-finite push-pop top-push pop-push push-non-empty StackSystem ;
end;

theorem Th2: :: STACKS_1:2
for X being non empty non void StackSystem st X is pop-finite holds
ex s being stack of X st emp s
proof
let X be non empty non void StackSystem ; ::_thesis: ( X is pop-finite implies ex s being stack of X st emp s )
assume A1: X is pop-finite ; ::_thesis: ex s being stack of X st emp s
set s1 = the stack of X;
defpred S1[ set , stack of X, stack of X] means $3 = pop $2;
A2: for n being Element of NAT
for x being stack of X ex y being stack of X st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of X such that
A3: ( f . 0 = the stack of X & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
consider i being Nat, s being stack of X such that
A4: ( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) by A1, Def8;
take  s ; ::_thesis: emp s
 i is Element of NAT by ORDINAL1:def_12;
hence  emp s by A3, A4; ::_thesis: verum
end;

registration
let X be non empty non void pop-finite StackSystem ;
cluster the s_empty of X ->  non empty ;
coherence
 not the s_empty of X is empty
proof
 ex s being stack of X st emp s by Th2;
hence  not the s_empty of X is empty by Def3; ::_thesis: verum
end;
end;

theorem Th3: :: STACKS_1:3
for X being non empty non void StackSystem
for s1, s2 being stack of X
for e1, e2 being Element of X st X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) holds
( e1 = e2 & s1 = s2 )
proof
let X be non empty non void StackSystem ; ::_thesis: for s1, s2 being stack of X
for e1, e2 being Element of X st X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) holds
( e1 = e2 & s1 = s2 )
let s1, s2 be stack of X; ::_thesis: for e1, e2 being Element of X st X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) holds
( e1 = e2 & s1 = s2 )
let e1, e2 be Element of X; ::_thesis: ( X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) implies ( e1 = e2 & s1 = s2 ) )
assume  X is top-push ; ::_thesis: ( not X is pop-push or not push (e1,s1) = push (e2,s2) or ( e1 = e2 & s1 = s2 ) )
then A1: ( e1 = top (push (e1,s1)) & e2 = top (push (e2,s2)) ) by Def10;
assume  X is pop-push ; ::_thesis: ( not push (e1,s1) = push (e2,s2) or ( e1 = e2 & s1 = s2 ) )
then  ( s1 = pop (push (e1,s1)) & s2 = pop (push (e2,s2)) ) by Def11;
hence  ( not push (e1,s1) = push (e2,s2) or ( e1 = e2 & s1 = s2 ) ) by A1; ::_thesis: verum
end;

theorem :: STACKS_1:4
for X being non empty non void StackSystem
for s1, s2 being stack of X st X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 holds
s1 = s2
proof
let X be non empty non void StackSystem ; ::_thesis: for s1, s2 being stack of X st X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 holds
s1 = s2
let s1, s2 be stack of X; ::_thesis: ( X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 implies s1 = s2 )
assume A1: X is push-pop ; ::_thesis: ( emp s1 or emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 )
assume  not emp s1 ; ::_thesis: ( emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 )
then  s1 = push ((top s1),(pop s1)) by A1, Def9;
hence  ( emp s2 or not pop s1 = pop s2 or not top s1 = top s2 or s1 = s2 ) by A1, Def9; ::_thesis: verum
end;

begin

scheme :: STACKS_1:sch 3
INDsch{ F1() ->  StackAlgebra, F2() ->  stack of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: for s being stack of F1() st emp s holds
P1[s] and
A2: for s being stack of F1()
for e being Element of F1() st P1[s] holds
P1[ push (e,s)]
proof
defpred S1[ set , stack of F1(), stack of F1()] means $3 = pop $2;
A3: for n being Element of NAT
for x being stack of F1() ex y being stack of F1() st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of F1() such that
A4: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A3);
consider i being Nat, s being stack of F1() such that
A5: ( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) by Def8;
defpred S2[ Nat] means P1[f . (i -' $1)];
 i -' 0 = i by NAT_D:40;
then A6: S2[ 0 ] by A5, A4, A1;
A7: now__::_thesis:_for_j_being_Nat_st_S2[j]_holds_
S2[j_+_1]
let j be Nat; ::_thesis: ( S2[j] implies S2[b1 + 1] )
assume A8: S2[j] ; ::_thesis: S2[b1 + 1]
A9: i -' (j + 1) = (i -' j) -' 1 by NAT_2:30;
percases ( i -' j >= 1 or i -' j < 0 + 1 ) ;
suppose i -' j >= 1 ; ::_thesis: S2[b1 + 1]
then  (i -' (j + 1)) + 1 = i -' j by A9, XREAL_1:235;
then  f . (i -' j) = pop (f . (i -' (j + 1))) by A4;
then  ( not emp f . (i -' (j + 1)) implies f . (i -' (j + 1)) = push ((top (f . (i -' (j + 1)))),(f . (i -' j))) ) by Def9;
hence  S2[j + 1] by A1, A2, A8; ::_thesis: verum
end;
supposeA10: i -' j < 0 + 1 ; ::_thesis: S2[b1 + 1]
then A11: i -' j <= 0 by NAT_1:13;
A12: i -' j = 0 by A10, NAT_1:13;
i -' (j + 1) = 0 -' 1 by A12, NAT_2:30
.= 0 by NAT_2:8 ;
hence  S2[j + 1] by A8, A11; ::_thesis: verum
end;
end;
end;
 for j being Nat holds S2[j] from NAT_1:sch_2(A6, A7);
then  S2[i] ;
hence  P1[F2()] by A4, XREAL_1:232; ::_thesis: verum
end;

scheme :: STACKS_1:sch 4
EXsch{ F1() ->  StackAlgebra, F2() ->  stack of F1(), F3() ->  non empty set , F4() ->  Element of F3(), F5( set , set ) ->  Element of F3() } :
 ex a being Element of F3() ex F being Function of the carrier' of F1(),F3() st
( a = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
proof
defpred S1[ set ] means ( ( for s being stack of F1() st emp s holds
[s,F4()] in $1 ) & ( for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in $1 holds
[(push (a,s)),F5(a,v)] in $1 ) );
consider M being set  such that
A1: for x being set holds
( x in M iff ( x in bool [: the carrier' of F1(),F3():] & S1[x] ) ) from XBOOLE_0:sch_1();
A2: ( S1[[: the carrier' of F1(),F3():]] & [: the carrier' of F1(),F3():] in bool [: the carrier' of F1(),F3():] ) by ZFMISC_1:def_1;
then A3: [: the carrier' of F1(),F3():] in M by A1;
reconsider M = M as non empty set by A1, A2;
set F = meet M;
reconsider F = meet M as Subset of [: the carrier' of F1(),F3():] by A3, SETFAM_1:3;
defpred S2[ stack of F1()] means  for y1, y2 being set st [$1,y1] in F & [$1,y2] in F holds
y1 = y2;
A4: S1[F]
proof
hereby  ::_thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let s be stack of F1(); ::_thesis: ( emp s implies [s,F4()] in F )
assume  emp s ; ::_thesis: [s,F4()] in F
then  for Y being set st Y in M holds
[s,F4()] in Y by A1;
hence  [s,F4()] in F by SETFAM_1:def_1; ::_thesis: verum
end;
let s be stack of F1(); ::_thesis: for a being Element of F1()
for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let a be Element of F1(); ::_thesis: for v being Element of F3() st [s,v] in F holds
[(push (a,s)),F5(a,v)] in F
let v be Element of F3(); ::_thesis: ( [s,v] in F implies [(push (a,s)),F5(a,v)] in F )
assume A5: [s,v] in F ; ::_thesis: [(push (a,s)),F5(a,v)] in F
now__::_thesis:_for_Y_being_set_st_Y_in_M_holds_
[(push_(a,s)),F5(a,v)]_in_Y
let Y be set ; ::_thesis: ( Y in M implies [(push (a,s)),F5(a,v)] in Y )
assume  Y in M ; ::_thesis: [(push (a,s)),F5(a,v)] in Y
then  ( S1[Y] & [s,v] in Y ) by A5, A1, SETFAM_1:def_1;
hence  [(push (a,s)),F5(a,v)] in Y ; ::_thesis: verum
end;
hence  [(push (a,s)),F5(a,v)] in F by SETFAM_1:def_1; ::_thesis: verum
end;
defpred S3[ stack of F1()] means  ex y being set st [$1,y] in F;
A6: for s being stack of F1() st emp s holds
S3[s]
proof
let s be stack of F1(); ::_thesis: ( emp s implies S3[s] )
assume A7: emp s ; ::_thesis: S3[s]
take y = F4(); ::_thesis: [s,y] in F
 for Y being set st Y in M holds
[s,F4()] in Y by A7, A1;
hence  [s,y] in F by SETFAM_1:def_1; ::_thesis: verum
end;
A8: for s being stack of F1()
for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
proof
let s be stack of F1(); ::_thesis: for e being Element of F1() st S3[s] holds
S3[ push (e,s)]
let e be Element of F1(); ::_thesis: ( S3[s] implies S3[ push (e,s)] )
given y being set  such that A9: [s,y] in F ; ::_thesis: S3[ push (e,s)]
reconsider y = y as Element of F3() by A9, ZFMISC_1:87;
take z = F5(e,y); ::_thesis: [(push (e,s)),z] in F
now__::_thesis:_for_Y_being_set_st_Y_in_M_holds_
[(push_(e,s)),z]_in_Y
let Y be set ; ::_thesis: ( Y in M implies [(push (e,s)),z] in Y )
assume A10: Y in M ; ::_thesis: [(push (e,s)),z] in Y
then  [s,y] in Y by A9, SETFAM_1:def_1;
hence  [(push (e,s)),z] in Y by A10, A1; ::_thesis: verum
end;
hence  [(push (e,s)),z] in F by SETFAM_1:def_1; ::_thesis: verum
end;
A11: for s being stack of F1() st emp s holds
S2[s]
proof
let s be stack of F1(); ::_thesis: ( emp s implies S2[s] )
assume A12: emp s ; ::_thesis: S2[s]
let y1, y2 be set ; ::_thesis: ( [s,y1] in F & [s,y2] in F implies y1 = y2 )
assume A13: ( [s,y1] in F & [s,y2] in F ) ; ::_thesis: y1 = y2
set Y1 = F \ {[s,y1]};
set Y2 = F \ {[s,y2]};
A14: now__::_thesis:_not_y1_<>_F4()
assume A15: y1 <> F4() ; ::_thesis: contradiction
 S1[F \ {[s,y1]}]
proof
hereby  ::_thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y1]}
let s1 be stack of F1(); ::_thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y1]} )
assume  emp s1 ; ::_thesis: [s1,F4()] in F \ {[s,y1]}
then A16: [s1,F4()] in F by A4;
 [s,y1] <> [s1,F4()] by A15, XTUPLE_0:1;
then  [s1,F4()] nin {[s,y1]} by TARSKI:def_1;
hence  [s1,F4()] in F \ {[s,y1]} by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
let s1 be stack of F1(); ::_thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let a be Element of F1(); ::_thesis: for v being Element of F3() st [s1,v] in F \ {[s,y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
let v be Element of F3(); ::_thesis: ( [s1,v] in F \ {[s,y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} )
assume  [s1,v] in F \ {[s,y1]} ; ::_thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y1]}
then  [s1,v] in F by XBOOLE_0:def_5;
then A17: [(push (a,s1)),F5(a,v)] in F by A4;
 push (a,s1) <> s by A12, Def12;
then  [s,y1] <> [(push (a,s1)),F5(a,v)] by XTUPLE_0:1;
then  [(push (a,s1)),F5(a,v)] nin {[s,y1]} by TARSKI:def_1;
hence  [(push (a,s1)),F5(a,v)] in F \ {[s,y1]} by A17, XBOOLE_0:def_5; ::_thesis: verum
end;
then  F \ {[s,y1]} in M by A1;
then  F c= F \ {[s,y1]} by SETFAM_1:3;
then  ( [s,y1] in F \ {[s,y1]} & [s,y1] in {[s,y1]} ) by A13, TARSKI:def_1;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_not_y2_<>_F4()
assume A18: y2 <> F4() ; ::_thesis: contradiction
 S1[F \ {[s,y2]}]
proof
hereby  ::_thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[s,y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[s,y2]}
let s1 be stack of F1(); ::_thesis: ( emp s1 implies [s1,F4()] in F \ {[s,y2]} )
assume  emp s1 ; ::_thesis: [s1,F4()] in F \ {[s,y2]}
then A19: [s1,F4()] in F by A4;
 [s,y2] <> [s1,F4()] by A18, XTUPLE_0:1;
then  [s1,F4()] nin {[s,y2]} by TARSKI:def_1;
hence  [s1,F4()] in F \ {[s,y2]} by A19, XBOOLE_0:def_5; ::_thesis: verum
end;
let s1 be stack of F1(); ::_thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let a be Element of F1(); ::_thesis: for v being Element of F3() st [s1,v] in F \ {[s,y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
let v be Element of F3(); ::_thesis: ( [s1,v] in F \ {[s,y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} )
assume  [s1,v] in F \ {[s,y2]} ; ::_thesis: [(push (a,s1)),F5(a,v)] in F \ {[s,y2]}
then  [s1,v] in F by XBOOLE_0:def_5;
then A20: [(push (a,s1)),F5(a,v)] in F by A4;
 push (a,s1) <> s by A12, Def12;
then  [s,y2] <> [(push (a,s1)),F5(a,v)] by XTUPLE_0:1;
then  [(push (a,s1)),F5(a,v)] nin {[s,y2]} by TARSKI:def_1;
hence  [(push (a,s1)),F5(a,v)] in F \ {[s,y2]} by A20, XBOOLE_0:def_5; ::_thesis: verum
end;
then  F \ {[s,y2]} in M by A1;
then  F c= F \ {[s,y2]} by SETFAM_1:3;
then  ( [s,y2] in F \ {[s,y2]} & [s,y2] in {[s,y2]} ) by A13, TARSKI:def_1;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  y1 = y2 by A14; ::_thesis: verum
end;
A21: for s being stack of F1()
for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
proof
let s be stack of F1(); ::_thesis: for e being Element of F1() st S2[s] holds
S2[ push (e,s)]
let e be Element of F1(); ::_thesis: ( S2[s] implies S2[ push (e,s)] )
assume A22: S2[s] ; ::_thesis: S2[ push (e,s)]
let y1, y2 be set ; ::_thesis: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F implies y1 = y2 )
assume A23: ( [(push (e,s)),y1] in F & [(push (e,s)),y2] in F ) ; ::_thesis: y1 = y2
 S3[s] from STACKS_1:sch_3(A6, A8);
then consider y being set  such that
A24: [s,y] in F ;
reconsider y = y as Element of F3() by A24, ZFMISC_1:87;
set Y1 = F \ {[(push (e,s)),y1]};
set Y2 = F \ {[(push (e,s)),y2]};
A25: now__::_thesis:_not_y1_<>_F5(e,y)
assume A26: y1 <> F5(e,y) ; ::_thesis: contradiction
 S1[F \ {[(push (e,s)),y1]}]
proof
hereby  ::_thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let s1 be stack of F1(); ::_thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y1]} )
assume A27: emp s1 ; ::_thesis: [s1,F4()] in F \ {[(push (e,s)),y1]}
then A28: [s1,F4()] in F by A4;
 not emp push (e,s) by Def12;
then  [(push (e,s)),y1] <> [s1,F4()] by A27, XTUPLE_0:1;
then  [s1,F4()] nin {[(push (e,s)),y1]} by TARSKI:def_1;
hence  [s1,F4()] in F \ {[(push (e,s)),y1]} by A28, XBOOLE_0:def_5; ::_thesis: verum
end;
let s1 be stack of F1(); ::_thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let a be Element of F1(); ::_thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y1]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
let v be Element of F3(); ::_thesis: ( [s1,v] in F \ {[(push (e,s)),y1]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} )
assume  [s1,v] in F \ {[(push (e,s)),y1]} ; ::_thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]}
then A29: [s1,v] in F by XBOOLE_0:def_5;
then A30: [(push (a,s1)),F5(a,v)] in F by A4;
now__::_thesis:_not_[(push_(e,s)),y1]_=_[(push_(a,s1)),F5(a,v)]
assume  [(push (e,s)),y1] = [(push (a,s1)),F5(a,v)] ; ::_thesis: contradiction
then A31: ( push (e,s) = push (a,s1) & y1 = F5(a,v) ) by XTUPLE_0:1;
then  ( e = a & s = s1 ) by Th3;
hence  contradiction by A22, A24, A29, A26, A31; ::_thesis: verum
end;
then  [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y1]} by TARSKI:def_1;
hence  [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y1]} by A30, XBOOLE_0:def_5; ::_thesis: verum
end;
then  F \ {[(push (e,s)),y1]} in M by A1;
then  F c= F \ {[(push (e,s)),y1]} by SETFAM_1:3;
then  ( [(push (e,s)),y1] in F \ {[(push (e,s)),y1]} & [(push (e,s)),y1] in {[(push (e,s)),y1]} ) by A23, TARSKI:def_1;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_not_y2_<>_F5(e,y)
assume A32: y2 <> F5(e,y) ; ::_thesis: contradiction
 S1[F \ {[(push (e,s)),y2]}]
proof
hereby  ::_thesis: for s being stack of F1()
for a being Element of F1()
for v being Element of F3() st [s,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let s1 be stack of F1(); ::_thesis: ( emp s1 implies [s1,F4()] in F \ {[(push (e,s)),y2]} )
assume A33: emp s1 ; ::_thesis: [s1,F4()] in F \ {[(push (e,s)),y2]}
then A34: [s1,F4()] in F by A4;
 not emp push (e,s) by Def12;
then  [(push (e,s)),y2] <> [s1,F4()] by A33, XTUPLE_0:1;
then  [s1,F4()] nin {[(push (e,s)),y2]} by TARSKI:def_1;
hence  [s1,F4()] in F \ {[(push (e,s)),y2]} by A34, XBOOLE_0:def_5; ::_thesis: verum
end;
let s1 be stack of F1(); ::_thesis: for a being Element of F1()
for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let a be Element of F1(); ::_thesis: for v being Element of F3() st [s1,v] in F \ {[(push (e,s)),y2]} holds
[(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
let v be Element of F3(); ::_thesis: ( [s1,v] in F \ {[(push (e,s)),y2]} implies [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} )
assume  [s1,v] in F \ {[(push (e,s)),y2]} ; ::_thesis: [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]}
then A35: [s1,v] in F by XBOOLE_0:def_5;
then A36: [(push (a,s1)),F5(a,v)] in F by A4;
now__::_thesis:_not_[(push_(e,s)),y2]_=_[(push_(a,s1)),F5(a,v)]
assume  [(push (e,s)),y2] = [(push (a,s1)),F5(a,v)] ; ::_thesis: contradiction
then A37: ( push (e,s) = push (a,s1) & y2 = F5(a,v) ) by XTUPLE_0:1;
then  ( e = a & s = s1 ) by Th3;
hence  contradiction by A22, A24, A35, A32, A37; ::_thesis: verum
end;
then  [(push (a,s1)),F5(a,v)] nin {[(push (e,s)),y2]} by TARSKI:def_1;
hence  [(push (a,s1)),F5(a,v)] in F \ {[(push (e,s)),y2]} by A36, XBOOLE_0:def_5; ::_thesis: verum
end;
then  F \ {[(push (e,s)),y2]} in M by A1;
then  F c= F \ {[(push (e,s)),y2]} by SETFAM_1:3;
then  ( [(push (e,s)),y2] in F \ {[(push (e,s)),y2]} & [(push (e,s)),y2] in {[(push (e,s)),y2]} ) by A23, TARSKI:def_1;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  y1 = y2 by A25; ::_thesis: verum
end;
A38: F is Function-like
proof
let x, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [x,y1] in F or not [x,y2] in F or y1 = y2 )
assume A39: ( [x,y1] in F & [x,y2] in F ) ; ::_thesis: y1 = y2
then reconsider x = x as stack of F1() by ZFMISC_1:87;
 S2[x] from STACKS_1:sch_3(A11, A21);
hence  y1 = y2 by A39; ::_thesis: verum
end;
 F is quasi_total
proof
percases ( F3() <> {} or F3() = {} ) ;
:: according to FUNCT_2:def_1
case F3() <> {} ; ::_thesis: the carrier' of F1() = dom F
thus  the carrier' of F1() c= dom F :: according to XBOOLE_0:def_10 ::_thesis: dom F c= the carrier' of F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of F1() or x in dom F )
assume  x in the carrier' of F1() ; ::_thesis: x in dom F
then reconsider x = x as stack of F1() ;
 S3[x] from STACKS_1:sch_3(A6, A8);
hence  x in dom F by XTUPLE_0:def_12; ::_thesis: verum
end;
thus  dom F c= the carrier' of F1() ; ::_thesis: verum
end;
case F3() = {} ; ::_thesis: F = {}
hence  F = {} ; ::_thesis: verum
end;
end;
end;
then reconsider F = F as Function of the carrier' of F1(),F3() by A38;
take a = F . F2(); ::_thesis: ex F being Function of the carrier' of F1(),F3() st
( a = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
take  F ; ::_thesis: ( a = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
thus  a = F . F2() ; ::_thesis: ( ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
hereby  ::_thesis: for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let s1 be stack of F1(); ::_thesis: ( emp s1 implies F . s1 = F4() )
assume  emp s1 ; ::_thesis: F . s1 = F4()
then  [s1,F4()] in F by A4;
hence  F . s1 = F4() by FUNCT_1:1; ::_thesis: verum
end;
let s1 be stack of F1(); ::_thesis: for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1))
let e be Element of F1(); ::_thesis: F . (push (e,s1)) = F5(e,(F . s1))
 dom F = the carrier' of F1() by FUNCT_2:def_1;
then  [s1,(F . s1)] in F by FUNCT_1:def_2;
then  [(push (e,s1)),F5(e,(F . s1))] in F by A4;
hence  F . (push (e,s1)) = F5(e,(F . s1)) by FUNCT_1:1; ::_thesis: verum
end;

scheme :: STACKS_1:sch 5
UNIQsch{ F1() ->  StackAlgebra, F2() ->  stack of F1(), F3() ->  non empty set , F4() ->  Element of F3(), F5( set , set ) ->  Element of F3() } :
 for a1, a2 being Element of F3() st ex F being Function of the carrier' of F1(),F3() st
( a1 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) & ex F being Function of the carrier' of F1(),F3() st
( a2 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) holds
a1 = a2
proof
let a1, a2 be Element of F3(); ::_thesis: ( ex F being Function of the carrier' of F1(),F3() st
( a1 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) & ex F being Function of the carrier' of F1(),F3() st
( a2 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) implies a1 = a2 )
given F1 being Function of the carrier' of F1(),F3() such that A1: ( a1 = F1 . F2() & ( for s1 being stack of F1() st emp s1 holds
F1 . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F1 . (push (e,s1)) = F5(e,(F1 . s1)) ) ) ; ::_thesis: ( for F being Function of the carrier' of F1(),F3() holds
( not a2 = F . F2() or ex s1 being stack of F1() st
( emp s1 & not F . s1 = F4() ) or ex s1 being stack of F1() ex e being Element of F1() st not F . (push (e,s1)) = F5(e,(F . s1)) ) or a1 = a2 )
given F2 being Function of the carrier' of F1(),F3() such that A2: ( a2 = F2 . F2() & ( for s1 being stack of F1() st emp s1 holds
F2 . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F2 . (push (e,s1)) = F5(e,(F2 . s1)) ) ) ; ::_thesis: a1 = a2
defpred S1[ stack of F1()] means F1 . $1 = F2 . $1;
A3: now__::_thesis:_for_s_being_stack_of_F1()_st_emp_s_holds_
S1[s]
let s be stack of F1(); ::_thesis: ( emp s implies S1[s] )
assume  emp s ; ::_thesis: S1[s]
then  ( F1 . s = F4() & F2 . s = F4() ) by A1, A2;
hence  S1[s] ; ::_thesis: verum
end;
A4: now__::_thesis:_for_s_being_stack_of_F1()
for_e_being_Element_of_F1()_st_S1[s]_holds_
S1[_push_(e,s)]
let s be stack of F1(); ::_thesis: for e being Element of F1() st S1[s] holds
S1[ push (e,s)]
let e be Element of F1(); ::_thesis: ( S1[s] implies S1[ push (e,s)] )
assume  S1[s] ; ::_thesis: S1[ push (e,s)]
then  F1 . (push (e,s)) = F5(e,(F2 . s)) by A1;
hence  S1[ push (e,s)] by A2; ::_thesis: verum
end;
 S1[F2()] from STACKS_1:sch_3(A3, A4);
hence  a1 = a2 by A1, A2; ::_thesis: verum
end;

begin


definition
let X be StackAlgebra;
let s be stack of X;
func|.s.| ->  Element of the carrier of X *  means :Def13: :: STACKS_1:def 13
 ex F being Function of the carrier' of X,( the carrier of X *) st
( it = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) );
existence
 ex b1 being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( b1 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) )
proof
deffunc H1( Element of X, Element of the carrier of X * ) ->  Element of the carrier of X * = <*$1*> ^ $2;
reconsider w = <*> the carrier of X as Element of the carrier of X * by FINSEQ_1:def_11;
 ex a being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( a = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = w ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = H1(e,F . s1) ) ) from STACKS_1:sch_4();
hence  ex b1 being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( b1 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st
( b1 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) & ex F being Function of the carrier' of X,( the carrier of X *) st
( b2 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) holds
b1 = b2
proof
deffunc H1( Element of X, Element of the carrier of X * ) ->  Element of the carrier of X * = <*$1*> ^ $2;
reconsider w = <*> the carrier of X as Element of the carrier of X * by FINSEQ_1:def_11;
 for a1, a2 being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st
( a1 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = w ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = H1(e,F . s1) ) ) & ex F being Function of the carrier' of X,( the carrier of X *) st
( a2 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = w ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = H1(e,F . s1) ) ) holds
a1 = a2 from STACKS_1:sch_5();
hence  for b1, b2 being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st
( b1 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) & ex F being Function of the carrier' of X,( the carrier of X *) st
( b2 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines |. STACKS_1:def_13_:_
 for X being StackAlgebra
for s being stack of X
for b3 being Element of the carrier of X * holds
( b3 = |.s.| iff ex F being Function of the carrier' of X,( the carrier of X *) st
( b3 = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) );

theorem Th5: :: STACKS_1:5
for X being StackAlgebra
for s being stack of X st emp s holds
|.s.| = {}
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st emp s holds
|.s.| = {}
let s be stack of X; ::_thesis: ( emp s implies |.s.| = {} )
 ex F being Function of the carrier' of X,( the carrier of X *) st
( |.s.| = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) by Def13;
hence  ( emp s implies |.s.| = {} ) ; ::_thesis: verum
end;

theorem Th6: :: STACKS_1:6
for X being StackAlgebra
for s being stack of X st not emp s holds
|.s.| = <*(top s)*> ^ |.(pop s).|
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st not emp s holds
|.s.| = <*(top s)*> ^ |.(pop s).|
let s be stack of X; ::_thesis: ( not emp s implies |.s.| = <*(top s)*> ^ |.(pop s).| )
consider F being Function of the carrier' of X,( the carrier of X *) such that
A1: ( |.s.| = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) by Def13;
A2: |.(pop s).| = F . (pop s) by A1, Def13;
assume  not emp s ; ::_thesis: |.s.| = <*(top s)*> ^ |.(pop s).|
then  s = push ((top s),(pop s)) by Def9;
hence  |.s.| = <*(top s)*> ^ |.(pop s).| by A1, A2; ::_thesis: verum
end;

theorem Th7: :: STACKS_1:7
for X being StackAlgebra
for s being stack of X st not emp s holds
|.(pop s).| = Del (|.s.|,1)
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st not emp s holds
|.(pop s).| = Del (|.s.|,1)
let s be stack of X; ::_thesis: ( not emp s implies |.(pop s).| = Del (|.s.|,1) )
assume  not emp s ; ::_thesis: |.(pop s).| = Del (|.s.|,1)
then  |.s.| = <*(top s)*> ^ |.(pop s).| by Th6;
hence  |.(pop s).| = Del (|.s.|,1) by WSIERP_1:40; ::_thesis: verum
end;

theorem Th8: :: STACKS_1:8
for X being StackAlgebra
for s being stack of X
for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
let s be stack of X; ::_thesis: for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
let e be Element of X; ::_thesis: |.(push (e,s)).| = <*e*> ^ |.s.|
 not emp push (e,s) by Def12;
hence |.(push (e,s)).| = <*(top (push (e,s)))*> ^ |.(pop (push (e,s))).| by Th6
.= <*e*> ^ |.(pop (push (e,s))).| by Def10
.= <*e*> ^ |.s.| by Def11 ;
::_thesis: verum
end;

theorem Th9: :: STACKS_1:9
for X being StackAlgebra
for s being stack of X st not emp s holds
top s = |.s.| . 1
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st not emp s holds
top s = |.s.| . 1
let s be stack of X; ::_thesis: ( not emp s implies top s = |.s.| . 1 )
assume  not emp s ; ::_thesis: top s = |.s.| . 1
then  |.s.| = <*(top s)*> ^ |.(pop s).| by Th6;
hence  top s = |.s.| . 1 by FINSEQ_1:41; ::_thesis: verum
end;

theorem Th10: :: STACKS_1:10
for X being StackAlgebra
for s being stack of X st |.s.| = {} holds
emp s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st |.s.| = {} holds
emp s
let s be stack of X; ::_thesis: ( |.s.| = {} implies emp s )
assume  ( |.s.| = {} & not emp s ) ; ::_thesis: contradiction
then  {} = <*(top s)*> ^ |.(pop s).| by Th6;
hence  contradiction ; ::_thesis: verum
end;

theorem Th11: :: STACKS_1:11
for A being non empty set
for s being stack of (StandardStackSystem A) holds |.s.| = s
proof
let A be non empty set ; ::_thesis: for s being stack of (StandardStackSystem A) holds |.s.| = s
defpred S1[ stack of (StandardStackSystem A)] means |.$1.| = $1;
A1: now__::_thesis:_for_s_being_stack_of_(StandardStackSystem_A)_st_emp_s_holds_
S1[s]
let s be stack of (StandardStackSystem A); ::_thesis: ( emp s implies S1[s] )
assume  emp s ; ::_thesis: S1[s]
then  ( s = {} & |.s.| = {} ) by Def7, Th5;
hence  S1[s] ; ::_thesis: verum
end;
A2: now__::_thesis:_for_s_being_stack_of_(StandardStackSystem_A)
for_e_being_Element_of_(StandardStackSystem_A)_st_S1[s]_holds_
S1[_push_(e,s)]
let s be stack of (StandardStackSystem A); ::_thesis: for e being Element of (StandardStackSystem A) st S1[s] holds
S1[ push (e,s)]
let e be Element of (StandardStackSystem A); ::_thesis: ( S1[s] implies S1[ push (e,s)] )
assume  S1[s] ; ::_thesis: S1[ push (e,s)]
then  |.(push (e,s)).| = <*e*> ^ s by Th8;
hence  S1[ push (e,s)] by Def7; ::_thesis: verum
end;
let s be stack of (StandardStackSystem A); ::_thesis: |.s.| = s
thus  S1[s] from STACKS_1:sch_3(A1, A2); ::_thesis: verum
end;

theorem Th12: :: STACKS_1:12
for X being StackAlgebra
for x being Element of the carrier of X * ex s being stack of X st |.s.| = x
proof
let X be StackAlgebra; ::_thesis: for x being Element of the carrier of X * ex s being stack of X st |.s.| = x
set D = the carrier of X;
defpred S1[ FinSequence of the carrier of X] means  ex s being stack of X st |.s.| = $1;
A1: S1[ <*> the carrier of X]
proof
consider s being stack of X such that
A2: emp s by Th2;
take  s ; ::_thesis: |.s.| = <*> the carrier of X
thus  |.s.| = <*> the carrier of X by A2, Th5; ::_thesis: verum
end;
A3: for p being FinSequence of the carrier of X
for x being Element of the carrier of X st S1[p] holds
S1[<*x*> ^ p]
proof
let p be FinSequence of the carrier of X; ::_thesis: for x being Element of the carrier of X st S1[p] holds
S1[<*x*> ^ p]
let x be Element of the carrier of X; ::_thesis: ( S1[p] implies S1[<*x*> ^ p] )
given s being stack of X such that A4: |.s.| = p ; ::_thesis: S1[<*x*> ^ p]
take s2 = push (x,s); ::_thesis: |.s2.| = <*x*> ^ p
thus  |.s2.| = <*x*> ^ p by A4, Th8; ::_thesis: verum
end;
 for p being FinSequence of the carrier of X holds S1[p] from STACKS_1:sch_1(A1, A3);
hence  for x being Element of the carrier of X * ex s being stack of X st |.s.| = x ; ::_thesis: verum
end;

definition
let X be StackAlgebra;
let s1, s2 be stack of X;
preds1 == s2 means :Def14: :: STACKS_1:def 14
|.s1.| = |.s2.|;
reflexivity
 for s1 being stack of X holds |.s1.| = |.s1.| ;
symmetry
 for s1, s2 being stack of X st |.s1.| = |.s2.| holds
|.s2.| = |.s1.| ;
end;

:: deftheorem Def14 defines == STACKS_1:def_14_:_
 for X being StackAlgebra
for s1, s2 being stack of X holds
( s1 == s2 iff |.s1.| = |.s2.| );

theorem Th13: :: STACKS_1:13
for X being StackAlgebra
for s1, s2, s3 being stack of X st s1 == s2 & s2 == s3 holds
s1 == s3
proof
let X be StackAlgebra; ::_thesis: for s1, s2, s3 being stack of X st s1 == s2 & s2 == s3 holds
s1 == s3
let s1, s2, s3 be stack of X; ::_thesis: ( s1 == s2 & s2 == s3 implies s1 == s3 )
assume  ( |.s1.| = |.s2.| & |.s2.| = |.s3.| ) ; :: according to STACKS_1:def_14 ::_thesis: s1 == s3
hence  |.s1.| = |.s3.| ; :: according to STACKS_1:def_14 ::_thesis: verum
end;

theorem Th14: :: STACKS_1:14
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & emp s1 holds
emp s2
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X st s1 == s2 & emp s1 holds
emp s2
let s1, s2 be stack of X; ::_thesis: ( s1 == s2 & emp s1 implies emp s2 )
assume A1: ( |.s1.| = |.s2.| & emp s1 ) ; :: according to STACKS_1:def_14 ::_thesis: emp s2
assume  not emp s2 ; ::_thesis: contradiction
then  |.s2.| = <*(top s2)*> ^ |.(pop s2).| by Th6;
hence  contradiction by A1, Th5; ::_thesis: verum
end;

theorem Th15: :: STACKS_1:15
for X being StackAlgebra
for s1, s2 being stack of X st emp s1 & emp s2 holds
s1 == s2
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X st emp s1 & emp s2 holds
s1 == s2
let s1, s2 be stack of X; ::_thesis: ( emp s1 & emp s2 implies s1 == s2 )
assume  ( emp s1 & emp s2 ) ; ::_thesis: s1 == s2
then  ( |.s1.| = {} & |.s2.| = {} ) by Th5;
hence  |.s1.| = |.s2.| ; :: according to STACKS_1:def_14 ::_thesis: verum
end;

theorem Th16: :: STACKS_1:16
for X being StackAlgebra
for s1, s2 being stack of X
for e being Element of X st s1 == s2 holds
push (e,s1) == push (e,s2)
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X
for e being Element of X st s1 == s2 holds
push (e,s1) == push (e,s2)
let s1, s2 be stack of X; ::_thesis: for e being Element of X st s1 == s2 holds
push (e,s1) == push (e,s2)
let e be Element of X; ::_thesis: ( s1 == s2 implies push (e,s1) == push (e,s2) )
assume  |.s1.| = |.s2.| ; :: according to STACKS_1:def_14 ::_thesis: push (e,s1) == push (e,s2)
hence |.(push (e,s1)).| = <*e*> ^ |.s2.| by Th8
.= |.(push (e,s2)).| by Th8 ;
:: according to STACKS_1:def_14 ::_thesis: verum
end;

theorem Th17: :: STACKS_1:17
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
pop s1 == pop s2
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
pop s1 == pop s2
let s1, s2 be stack of X; ::_thesis: ( s1 == s2 & not emp s1 implies pop s1 == pop s2 )
assume A1: ( s1 == s2 & not emp s1 ) ; ::_thesis: pop s1 == pop s2
then A2: ( |.s1.| = |.s2.| & not emp s2 ) by Def14, Th14;
thus |.(pop s1).| = Del (|.s1.|,1) by A1, Th7
.= |.(pop s2).| by A2, Th7 ; :: according to STACKS_1:def_14 ::_thesis: verum
end;

theorem Th18: :: STACKS_1:18
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
top s1 = top s2
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
top s1 = top s2
let s1, s2 be stack of X; ::_thesis: ( s1 == s2 & not emp s1 implies top s1 = top s2 )
assume A1: ( s1 == s2 & not emp s1 ) ; ::_thesis: top s1 = top s2
then A2: ( |.s1.| = |.s2.| & not emp s2 ) by Def14, Th14;
thus  top s1 = |.s1.| . 1 by A1, Th9
.= top s2 by A2, Th9 ; ::_thesis: verum
end;

definition
let X be StackAlgebra;
attrX is proper-for-identity  means :Def15: :: STACKS_1:def 15
 for s1, s2 being stack of X st s1 == s2 holds
s1 = s2;
end;

:: deftheorem Def15 defines proper-for-identity STACKS_1:def_15_:_
 for X being StackAlgebra holds
( X is proper-for-identity iff for s1, s2 being stack of X st s1 == s2 holds
s1 = s2 );

registration
let A be non empty set ;
cluster StandardStackSystem A ->  non empty non void strict proper-for-identity ;
coherence
 StandardStackSystem A is proper-for-identity
proof
set X = StandardStackSystem A;
let s1, s2 be stack of (StandardStackSystem A); :: according to STACKS_1:def_15 ::_thesis: ( s1 == s2 implies s1 = s2 )
assume  |.s1.| = |.s2.| ; :: according to STACKS_1:def_14 ::_thesis: s1 = s2
hence s1 = |.s2.| by Th11
.= s2 by Th11 ;
::_thesis: verum
end;
end;

definition
let X be StackAlgebra;
func ==_ X ->  Relation of the carrier' of X means :Def16: :: STACKS_1:def 16
 for s1, s2 being stack of X holds
( [s1,s2] in it iff s1 == s2 );
existence
 ex b1 being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in b1 iff s1 == s2 )
proof
defpred S1[ stack of X, stack of X] means $1 == $2;
thus  ex R being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in R iff S1[s1,s2] ) from RELSET_1:sch_2(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of the carrier' of X st ( for s1, s2 being stack of X holds
( [s1,s2] in b1 iff s1 == s2 ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in b2 iff s1 == s2 ) ) holds
b1 = b2
proof
defpred S1[ stack of X, stack of X] means $1 == $2;
let R1, R2 be Relation of the carrier' of X; ::_thesis: ( ( for s1, s2 being stack of X holds
( [s1,s2] in R1 iff s1 == s2 ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in R2 iff s1 == s2 ) ) implies R1 = R2 )
assume that
A1: for s1, s2 being stack of X holds
( [s1,s2] in R1 iff S1[s1,s2] ) and
A2: for s1, s2 being stack of X holds
( [s1,s2] in R2 iff S1[s1,s2] ) ; ::_thesis: R1 = R2
thus  R1 = R2 from RELSET_1:sch_4(A1, A2); ::_thesis: verum
end;
end;

:: deftheorem Def16 defines ==_ STACKS_1:def_16_:_
 for X being StackAlgebra
for b2 being Relation of the carrier' of X holds
( b2 = ==_ X iff for s1, s2 being stack of X holds
( [s1,s2] in b2 iff s1 == s2 ) );

registration
let X be StackAlgebra;
cluster ==_ X ->  total symmetric transitive ;
coherence
 ( ==_ X is total & ==_ X is symmetric & ==_ X is transitive )
proof
set R = ==_ X;
thus A1: dom (==_ X) = the carrier' of X :: according to PARTFUN1:def_2 ::_thesis: ( ==_ X is symmetric & ==_ X is transitive )
proof
thus  dom (==_ X) c= the carrier' of X ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of X c= dom (==_ X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of X or x in dom (==_ X) )
assume  x in the carrier' of X ; ::_thesis: x in dom (==_ X)
then reconsider s = x as stack of X ;
 [s,s] in ==_ X by Def16;
hence  x in dom (==_ X) by XTUPLE_0:def_12; ::_thesis: verum
end;
A2: field (==_ X) = (dom (==_ X)) \/ (rng (==_ X))
.= the carrier' of X by A1, XBOOLE_1:12 ;
thus  ==_ X is symmetric ::_thesis: ==_ X is transitive
proof
let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field (==_ X) or not y in field (==_ X) or not [x,y] in ==_ X or [y,x] in ==_ X )
assume  ( x in field (==_ X) & y in field (==_ X) ) ; ::_thesis: ( not [x,y] in ==_ X or [y,x] in ==_ X )
then reconsider s1 = x, s2 = y as stack of X by A2;
assume  [x,y] in ==_ X ; ::_thesis: [y,x] in ==_ X
then  s1 == s2 by Def16;
hence  [y,x] in ==_ X by Def16; ::_thesis: verum
end;
let x, y, z be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not x in field (==_ X) or not y in field (==_ X) or not z in field (==_ X) or not [x,y] in ==_ X or not [y,z] in ==_ X or [x,z] in ==_ X )
assume  ( x in field (==_ X) & y in field (==_ X) & z in field (==_ X) ) ; ::_thesis: ( not [x,y] in ==_ X or not [y,z] in ==_ X or [x,z] in ==_ X )
then reconsider s1 = x, s2 = y, s3 = z as stack of X by A2;
assume  ( [x,y] in ==_ X & [y,z] in ==_ X ) ; ::_thesis: [x,z] in ==_ X
then  ( s1 == s2 & s2 == s3 ) by Def16;
then  s1 == s3 by Th13;
hence  [x,z] in ==_ X by Def16; ::_thesis: verum
end;
end;

theorem Th19: :: STACKS_1:19
for X being StackAlgebra
for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
let s be stack of X; ::_thesis: ( emp s implies Class ((==_ X),s) = the s_empty of X )
assume A1: emp s ; ::_thesis: Class ((==_ X),s) = the s_empty of X
thus  Class ((==_ X),s) c= the s_empty of X :: according to XBOOLE_0:def_10 ::_thesis: the s_empty of X c= Class ((==_ X),s)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Class ((==_ X),s) or x in the s_empty of X )
assume A2: x in Class ((==_ X),s) ; ::_thesis: x in the s_empty of X
then reconsider s1 = x as stack of X ;
 [s,s1] in ==_ X by A2, EQREL_1:18;
then  s == s1 by Def16;
then  emp s1 by A1, Th14;
hence  x in the s_empty of X by Def3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the s_empty of X or x in Class ((==_ X),s) )
assume A3: x in the s_empty of X ; ::_thesis: x in Class ((==_ X),s)
then reconsider s1 = x as stack of X ;
 emp s1 by A3, Def3;
then  s == s1 by A1, Th15;
then  [s,s1] in ==_ X by Def16;
hence  x in Class ((==_ X),s) by EQREL_1:18; ::_thesis: verum
end;

definition
let X be StackAlgebra;
let s be stack of X;
func coset s ->  Subset of the carrier' of X means :Def17: :: STACKS_1:def 17
( s in it & ( for e being Element of X
for s1 being stack of X st s1 in it holds
( push (e,s1) in it & ( not emp s1 implies pop s1 in it ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
it c= A ) );
existence
 ex b1 being Subset of the carrier' of X st
( s in b1 & ( for e being Element of X
for s1 being stack of X st s1 in b1 holds
( push (e,s1) in b1 & ( not emp s1 implies pop s1 in b1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
b1 c= A ) )
proof
defpred S1[ set ] means ( s in $1 & ( for e being Element of X
for s1 being stack of X st s1 in $1 holds
( push (e,s1) in $1 & ( not emp s1 implies pop s1 in $1 ) ) ) );
consider Y being set  such that
A1: for x being set holds
( x in Y iff ( x in bool the carrier' of X & S1[x] ) ) from XBOOLE_0:sch_1();
set S = the carrier' of X;
A2: ( S1[ the carrier' of X] & the carrier' of X in bool the carrier' of X ) by ZFMISC_1:def_1;
then A3: the carrier' of X in Y by A1;
reconsider Y = Y as non empty set by A2, A1;
reconsider C = meet Y as Subset of the carrier' of X by A3, SETFAM_1:3;
take  C ; ::_thesis: ( s in C & ( for e being Element of X
for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C c= A ) )
 for x being set st x in Y holds
s in x by A1;
hence  s in C by SETFAM_1:def_1; ::_thesis: ( ( for e being Element of X
for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C c= A ) )
hereby  ::_thesis: for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C c= A
let e be Element of X; ::_thesis: for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) )
let s1 be stack of X; ::_thesis: ( s1 in C implies ( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) )
assume A4: s1 in C ; ::_thesis: ( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) )
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
push_(e,s1)_in_x
let x be set ; ::_thesis: ( x in Y implies push (e,s1) in x )
assume A5: x in Y ; ::_thesis: push (e,s1) in x
then  s1 in x by A4, SETFAM_1:def_1;
hence  push (e,s1) in x by A1, A5; ::_thesis: verum
end;
hence  push (e,s1) in C by SETFAM_1:def_1; ::_thesis: ( not emp s1 implies pop s1 in C )
assume A6: not emp s1 ; ::_thesis: pop s1 in C
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
pop_s1_in_x
let x be set ; ::_thesis: ( x in Y implies pop s1 in x )
assume A7: x in Y ; ::_thesis: pop s1 in x
then  s1 in x by A4, SETFAM_1:def_1;
hence  pop s1 in x by A1, A6, A7; ::_thesis: verum
end;
hence  pop s1 in C by SETFAM_1:def_1; ::_thesis: verum
end;
let A be Subset of the carrier' of X; ::_thesis: ( s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) implies C c= A )
assume  S1[A] ; ::_thesis: C c= A
then  A in Y by A1;
hence  C c= A by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of the carrier' of X st s in b1 & ( for e being Element of X
for s1 being stack of X st s1 in b1 holds
( push (e,s1) in b1 & ( not emp s1 implies pop s1 in b1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
b1 c= A ) & s in b2 & ( for e being Element of X
for s1 being stack of X st s1 in b2 holds
( push (e,s1) in b2 & ( not emp s1 implies pop s1 in b2 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
b2 c= A ) holds
b1 = b2
proof
let C1, C2 be Subset of the carrier' of X; ::_thesis: ( s in C1 & ( for e being Element of X
for s1 being stack of X st s1 in C1 holds
( push (e,s1) in C1 & ( not emp s1 implies pop s1 in C1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C1 c= A ) & s in C2 & ( for e being Element of X
for s1 being stack of X st s1 in C2 holds
( push (e,s1) in C2 & ( not emp s1 implies pop s1 in C2 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C2 c= A ) implies C1 = C2 )
assume A8: ( s in C1 & ( for e being Element of X
for s1 being stack of X st s1 in C1 holds
( push (e,s1) in C1 & ( not emp s1 implies pop s1 in C1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C1 c= A ) & s in C2 & ( for e being Element of X
for s1 being stack of X st s1 in C2 holds
( push (e,s1) in C2 & ( not emp s1 implies pop s1 in C2 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C2 c= A ) & not C1 = C2 ) ; ::_thesis: contradiction
 C1 = C2
proof
thus  ( C1 c= C2 & C2 c= C1 ) by A8; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
hence  contradiction by A8; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines coset STACKS_1:def_17_:_
 for X being StackAlgebra
for s being stack of X
for b3 being Subset of the carrier' of X holds
( b3 = coset s iff ( s in b3 & ( for e being Element of X
for s1 being stack of X st s1 in b3 holds
( push (e,s1) in b3 & ( not emp s1 implies pop s1 in b3 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
b3 c= A ) ) );

theorem Th20: :: STACKS_1:20
for X being StackAlgebra
for s, s1 being stack of X
for e being Element of X holds
( ( push (e,s) in coset s1 implies s in coset s1 ) & ( not emp s & pop s in coset s1 implies s in coset s1 ) )
proof
let X be StackAlgebra; ::_thesis: for s, s1 being stack of X
for e being Element of X holds
( ( push (e,s) in coset s1 implies s in coset s1 ) & ( not emp s & pop s in coset s1 implies s in coset s1 ) )
let s, s1 be stack of X; ::_thesis: for e being Element of X holds
( ( push (e,s) in coset s1 implies s in coset s1 ) & ( not emp s & pop s in coset s1 implies s in coset s1 ) )
let e be Element of X; ::_thesis: ( ( push (e,s) in coset s1 implies s in coset s1 ) & ( not emp s & pop s in coset s1 implies s in coset s1 ) )
 ( pop (push (e,s)) = s & not emp push (e,s) ) by Def11, Def12;
hence  ( push (e,s) in coset s1 implies s in coset s1 ) by Def17; ::_thesis: ( not emp s & pop s in coset s1 implies s in coset s1 )
assume  not emp s ; ::_thesis: ( not pop s in coset s1 or s in coset s1 )
then  push ((top s),(pop s)) = s by Def9;
hence  ( not pop s in coset s1 or s in coset s1 ) by Def17; ::_thesis: verum
end;

theorem :: STACKS_1:21
for X being StackAlgebra
for s being stack of X
for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
let s be stack of X; ::_thesis: for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
let e be Element of X; ::_thesis: ( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
 ( pop (push (e,s)) = s & not emp push (e,s) & push (e,s) in coset (push (e,s)) ) by Def11, Def12, Def17;
hence  s in coset (push (e,s)) by Def17; ::_thesis: ( not emp s implies s in coset (pop s) )
assume  not emp s ; ::_thesis: s in coset (pop s)
then  ( push ((top s),(pop s)) = s & pop s in coset (pop s) ) by Def9, Def17;
hence  s in coset (pop s) by Def17; ::_thesis: verum
end;

theorem :: STACKS_1:22
for X being StackAlgebra
for s being stack of X ex s1 being stack of X st
( emp s1 & s1 in coset s )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X ex s1 being stack of X st
( emp s1 & s1 in coset s )
let s be stack of X; ::_thesis: ex s1 being stack of X st
( emp s1 & s1 in coset s )
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 Element of NAT
for x being stack of X ex y being stack of X st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of X such that
A2: ( f . 0 = s & ( for i being Element of NAT holds S1[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch_2(A1);
defpred S2[ Nat] means f . $1 in coset s;
A3: S2[ 0 ] by A2, Def17;
A4: now__::_thesis:_for_i_being_Nat_st_S2[i]_holds_
S2[i_+_1]
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A5: S2[i] ; ::_thesis: S2[i + 1]
 i in NAT by ORDINAL1:def_12;
then  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;
then  ( f . (i + 1) = s or ( not emp f . i & f . (i + 1) = pop (f . i) ) ) by Def3;
hence  S2[i + 1] by A5, Def17; ::_thesis: verum
end;
A6: for i being Nat holds S2[i] from NAT_1:sch_2(A3, A4);
consider i being Nat, s1 being stack of X such that
A7: ( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) ) by Def8;
take  s1 ; ::_thesis: ( emp s1 & s1 in coset s )
 i in NAT by ORDINAL1:def_12;
then  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 & s1 in coset s ) by A7, A6, Def3; ::_thesis: verum
end;

registration
let A be non empty set ;
let R be Relation of A;
cluster Relation-like NAT -defined A -valued Function-like non empty V46() FinSequence-like FinSubsequence-like for RedSequence of R;
existence
 ex b1 being RedSequence of R st b1 is A -valued
proof
set a = the Element of A;
reconsider t = <* the Element of A*> as RedSequence of R by REWRITE1:6;
take  t ; ::_thesis: t is A -valued
thus  t is A -valued ; ::_thesis: verum
end;
end;

definition
let X be StackAlgebra;
func ConstructionRed X ->  Relation of the carrier' of X means :Def18: :: STACKS_1:def 18
 for s1, s2 being stack of X holds
( [s1,s2] in it iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) );
existence
 ex b1 being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in b1 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) )
proof
defpred S1[ stack of X, stack of X] means ( ( not emp $1 & $2 = pop $1 ) or ex e being Element of X st $2 = push (e,$1) );
thus  ex R being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in R iff S1[s1,s2] ) from RELSET_1:sch_2(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of the carrier' of X st ( for s1, s2 being stack of X holds
( [s1,s2] in b1 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in b2 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) holds
b1 = b2
proof
defpred S1[ stack of X, stack of X] means ( ( not emp $1 & $2 = pop $1 ) or ex e being Element of X st $2 = push (e,$1) );
let R1, R2 be Relation of the carrier' of X; ::_thesis: ( ( for s1, s2 being stack of X holds
( [s1,s2] in R1 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in R2 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) implies R1 = R2 )
assume that
A1: for s1, s2 being stack of X holds
( [s1,s2] in R1 iff S1[s1,s2] ) and
A2: for s1, s2 being stack of X holds
( [s1,s2] in R2 iff S1[s1,s2] ) ; ::_thesis: R1 = R2
thus  R1 = R2 from RELSET_1:sch_4(A1, A2); ::_thesis: verum
end;
end;

:: deftheorem Def18 defines ConstructionRed STACKS_1:def_18_:_
 for X being StackAlgebra
for b2 being Relation of the carrier' of X holds
( b2 = ConstructionRed X iff for s1, s2 being stack of X holds
( [s1,s2] in b2 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) );

theorem Th23: :: STACKS_1:23
for A being non empty set
for R being Relation of A
for t being RedSequence of R holds
( t . 1 in A iff t is A -valued )
proof
let A be non empty set ; ::_thesis: for R being Relation of A
for t being RedSequence of R holds
( t . 1 in A iff t is A -valued )
let R be Relation of A; ::_thesis: for t being RedSequence of R holds
( t . 1 in A iff t is A -valued )
let t be RedSequence of R; ::_thesis: ( t . 1 in A iff t is A -valued )
 rng t <> {} ;
then  1 in dom t by FINSEQ_3:32;
then A1: t . 1 in rng t by FUNCT_1:def_3;
hereby  ::_thesis: ( t is A -valued implies t . 1 in A )
assume A2: t . 1 in A ; ::_thesis: t is A -valued
defpred S1[ Nat] means ( $1 in dom t implies t . $1 in A );
A3: S1[ 0 ] by FINSEQ_3:24;
A4: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume  S1[i] ; ::_thesis: S1[i + 1]
assume A5: ( i + 1 in dom t & t . (i + 1) nin A ) ; ::_thesis: contradiction
 ( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A6: i = j + 1 by A2, A5, NAT_1:6;
 ( i <= i + 1 & i + 1 <= len t ) by A5, FINSEQ_3:25, NAT_1:11;
then  ( 1 <= i & i <= len t ) by A6, NAT_1:11, XXREAL_0:2;
then  i in dom t by FINSEQ_3:25;
then  [(t . i),(t . (i + 1))] in R by A5, REWRITE1:def_2;
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
A7: for i being Nat holds S1[i] from NAT_1:sch_2(A3, A4);
thus  t is A -valued ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not x in rng t or x in A )
assume  x in rng t ; ::_thesis: x in A
then consider y being set  such that
A8: ( y in dom t & x = t . y ) by FUNCT_1:def_3;
reconsider y = y as Nat by A8;
thus  x in A by A8, A7; ::_thesis: verum
end;
end;
assume  rng t c= A ; :: according to RELAT_1:def_19 ::_thesis: t . 1 in A
hence  t . 1 in A by A1; ::_thesis: verum
end;

scheme :: STACKS_1:sch 6
PathIND{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Element of F1(), F4() ->  Relation of F1(), P1[ set ] } :
 P1[F3()]
provided
A1: P1[F2()] and
A2: F4() reduces F2(),F3() and
A3: for x, y being Element of F1() st F4() reduces F2(),x & [x,y] in F4() & P1[x] holds
P1[y]
proof
consider t being RedSequence of F4() such that
A4: ( t . 1 = F2() & t . (len t) = F3() ) by A2, REWRITE1:def_3;
reconsider t = t as F1() -valued RedSequence of F4() by A4, Th23;
defpred S1[ Nat] means ( $1 in dom t implies P1[t . $1] );
A5: S1[ 0 ] by FINSEQ_3:24;
A6: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
proof
assume A8: ( i + 1 in dom t & P1[t . (i + 1)] ) ; ::_thesis: contradiction
 ( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A9: i = j + 1 by A1, A4, A8, NAT_1:6;
 ( i <= i + 1 & i + 1 <= len t ) by A8, FINSEQ_3:25, NAT_1:11;
then A10: ( 1 <= i & i <= len t & rng t <> {} ) by A9, NAT_1:11, XXREAL_0:2;
then A11: ( i in dom t & 1 in dom t ) by FINSEQ_3:25, FINSEQ_3:32;
A12: ( t . i = t /. i & t . (i + 1) = t /. (i + 1) ) by A8, A11, PARTFUN1:def_6;
then  [(t /. i),(t /. (i + 1))] in F4() by A8, A11, REWRITE1:def_2;
hence  contradiction by A3, A7, A8, A11, A4, A10, A12, REWRITE1:17; ::_thesis: verum
end;
end;
A13: for i being Nat holds S1[i] from NAT_1:sch_2(A5, A6);
 len t in dom t by FINSEQ_5:6;
hence  P1[F3()] by A4, A13; ::_thesis: verum
end;

theorem Th24: :: STACKS_1:24
for X being StackAlgebra
for s being stack of X
for t being RedSequence of ConstructionRed X st s = t . 1 holds
rng t c= coset s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for t being RedSequence of ConstructionRed X st s = t . 1 holds
rng t c= coset s
let s be stack of X; ::_thesis: for t being RedSequence of ConstructionRed X st s = t . 1 holds
rng t c= coset s
set R = ConstructionRed X;
let t be RedSequence of ConstructionRed X; ::_thesis: ( s = t . 1 implies rng t c= coset s )
assume A1: s = t . 1 ; ::_thesis: rng t c= coset s
then reconsider u = t as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
defpred S1[ Nat] means ( $1 in dom t implies t . $1 in coset s );
A2: S1[ 0 ] by FINSEQ_3:24;
A3: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
proof
assume A5: ( i + 1 in dom t & t . (i + 1) nin coset s ) ; ::_thesis: contradiction
 ( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A6: i = j + 1 by A1, A5, Def17, NAT_1:6;
 ( i <= i + 1 & i + 1 <= len t ) by A5, FINSEQ_3:25, NAT_1:11;
then A7: ( 1 <= i & i <= len t & rng t <> {} ) by A6, NAT_1:11, XXREAL_0:2;
then A8: ( i in dom t & 1 in dom t ) by FINSEQ_3:25, FINSEQ_3:32;
then A9: ( t . i = u /. i & t . (i + 1) = u /. (i + 1) ) by A5, PARTFUN1:def_6;
then  [(u /. i),(u /. (i + 1))] in ConstructionRed X by A5, A8, REWRITE1:def_2;
then  ( ( not emp u /. i & u /. (i + 1) = pop (u /. i) ) or ex e being Element of X st u /. (i + 1) = push (e,(u /. i)) ) by Def18;
hence  contradiction by A4, A5, A7, A9, Def17, FINSEQ_3:25; ::_thesis: verum
end;
end;
A10: for i being Nat holds S1[i] from NAT_1:sch_2(A2, A3);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng t or x in coset s )
assume  x in rng t ; ::_thesis: x in coset s
then  ex y being set st
( y in dom t & x = t . y ) by FUNCT_1:def_3;
hence  x in coset s by A10; ::_thesis: verum
end;

theorem Th25: :: STACKS_1:25
for X being StackAlgebra
for s being stack of X holds coset s =  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }
proof
let X be StackAlgebra; ::_thesis: for s being stack of X holds coset s =  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }
let s be stack of X; ::_thesis: coset s =  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }
set R = ConstructionRed X;
A1:  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  c= the carrier' of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  or x in the carrier' of X )
assume  x in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ; ::_thesis: x in the carrier' of X
then  ex s1 being stack of X st
( x = s1 & ConstructionRed X reduces s,s1 ) ;
hence  x in the carrier' of X ; ::_thesis: verum
end;
 ConstructionRed X reduces s,s by REWRITE1:12;
then A2: s in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ;
now__::_thesis:_for_e_being_Element_of_X
for_s2_being_stack_of_X_st_s2_in__{__s1_where_s1_is_stack_of_X_:_ConstructionRed_X_reduces_s,s1__}__holds_
(_push_(e,s2)_in__{__s1_where_s1_is_stack_of_X_:_ConstructionRed_X_reduces_s,s1__}__&_(_not_emp_s2_implies_pop_s2_in__{__s1_where_s1_is_stack_of_X_:_ConstructionRed_X_reduces_s,s1__}__)_)
let e be Element of X; ::_thesis: for s2 being stack of X st s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  holds
( push (e,s2) in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  & ( not emp s2 implies pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ) )
let s2 be stack of X; ::_thesis: ( s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  implies ( push (e,s2) in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  & ( not emp s2 implies pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ) ) )
assume  s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ; ::_thesis: ( push (e,s2) in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  & ( not emp s2 implies pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ) )
then A3: ex s1 being stack of X st
( s2 = s1 & ConstructionRed X reduces s,s1 ) ;
 [s2,(push (e,s2))] in ConstructionRed X by Def18;
then  ConstructionRed X reduces s2, push (e,s2) by REWRITE1:15;
then  ConstructionRed X reduces s, push (e,s2) by A3, REWRITE1:16;
hence  push (e,s2) in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ; ::_thesis: ( not emp s2 implies pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  )
assume  not emp s2 ; ::_thesis: pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }
then  [s2,(pop s2)] in ConstructionRed X by Def18;
then  ConstructionRed X reduces s2, pop s2 by REWRITE1:15;
then  ConstructionRed X reduces s, pop s2 by A3, REWRITE1:16;
hence  pop s2 in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ; ::_thesis: verum
end;
hence  coset s c=  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  by A1, A2, Def17; :: according to XBOOLE_0:def_10 ::_thesis:  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  c= coset s
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  or x in coset s )
assume  x in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ; ::_thesis: x in coset s
then consider s1 being stack of X such that
A4: ( x = s1 & ConstructionRed X reduces s,s1 ) ;
consider t being RedSequence of ConstructionRed X such that
A5: ( s = t . 1 & s1 = t . (len t) ) by A4, REWRITE1:def_3;
 len t in dom t by FINSEQ_5:6;
then  ( x in rng t & rng t c= coset s ) by A4, A5, Th24, FUNCT_1:def_3;
hence  x in coset s ; ::_thesis: verum
end;

definition
let X be StackAlgebra;
let s be stack of X;
func core s ->  stack of X means :Def19: :: STACKS_1:def 19
( emp it & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = it & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) );
existence
 ex b1 being stack of X st
( emp b1 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) )
proof
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 Element of NAT
for x being stack of X ex y being stack of X st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of X such that
A2: ( f . 0 = s & ( for i being Element of 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 ; ::_thesis: ( 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) ) ) ) )
 i in NAT by ORDINAL1:def_12;
then  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, Def3; ::_thesis: 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; :: according to REWRITE1:def_2 ::_thesis: for b1 being Element of NAT 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 Element of NAT ; ::_thesis: ( 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 ) ; ::_thesis: [(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 by Def3;
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; ::_thesis: 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 ; ::_thesis: ( 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; ::_thesis: ( 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 ;
::_thesis: 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; ::_thesis: ( 1 <= k & k < len t implies ( not emp t /. k & t /. (k + 1) = pop (t /. k) ) )
assume A14: ( 1 <= k & k < len t ) ; ::_thesis: ( 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; ::_thesis: t /. (k + 1) = pop (t /. k)
then A18: t /. k nin the s_empty of X by Def3;
 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; ::_thesis: verum
end;
uniqueness
 for b1, b2 being stack of X st emp b1 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp b2 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b2 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) holds
b1 = b2
proof
let x1, x2 be stack of X; ::_thesis: ( emp x1 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = x1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp x2 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = x2 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) implies x1 = x2 )
assume A19: emp x1 ; ::_thesis: ( for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x1 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or not emp x2 or for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
given t1 being the carrier' of X -valued RedSequence of ConstructionRed X such that A20: ( t1 . 1 = s & t1 . (len t1) = x1 ) and
A21: for i being Nat st 1 <= i & i < len t1 holds
( not emp t1 /. i & t1 /. (i + 1) = pop (t1 /. i) ) ; ::_thesis: ( not emp x2 or for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
assume A22: emp x2 ; ::_thesis: ( for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
given t2 being the carrier' of X -valued RedSequence of ConstructionRed X such that A23: ( t2 . 1 = s & t2 . (len t2) = x2 ) and
A24: for i being Nat st 1 <= i & i < len t2 holds
( not emp t2 /. i & t2 /. (i + 1) = pop (t2 /. i) ) ; ::_thesis: x1 = x2
A25: ( len t1 in dom t1 & len t2 in dom t2 & 1 in dom t1 & 1 in dom t2 ) by FINSEQ_5:6;
defpred S1[ Nat] means ( ( $1 in dom t1 implies $1 in dom t2 ) & ( $1 in dom t2 implies $1 in dom t1 ) & ( $1 in dom t1 implies t1 . $1 = t2 . $1 ) );
A26: S1[ 0 ] by FINSEQ_3:24;
A27: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A28: S1[i] ; ::_thesis: S1[i + 1]
percases ( i = 0 or ex j being Nat st i = j + 1 ) by NAT_1:6;
suppose i = 0 ; ::_thesis: S1[i + 1]
hence  S1[i + 1] by A20, A23, FINSEQ_5:6; ::_thesis: verum
end;
suppose ex j being Nat st i = j + 1 ; ::_thesis: S1[i + 1]
then consider j being Nat such that
A29: i = j + 1 ;
A30: i >= 1 by A29, NAT_1:11;
hereby  ::_thesis: ( i + 1 in dom t2 iff i + 1 in dom t1 )
assume  i + 1 in dom t1 ; ::_thesis: i + 1 in dom t2
then  i + 1 <= len t1 by FINSEQ_3:25;
then  i < len t1 by NAT_1:13;
then  ( i in dom t1 & not emp t1 /. i ) by A21, A30, FINSEQ_3:25;
then  ( len t2 <> i & i <= len t2 ) by A22, A23, A28, FINSEQ_3:25, PARTFUN1:def_6;
then  i < len t2 by XXREAL_0:1;
then  ( 1 <= i + 1 & i + 1 <= len t2 ) by NAT_1:11, NAT_1:13;
hence  i + 1 in dom t2 by FINSEQ_3:25; ::_thesis: verum
end;
hereby  ::_thesis: ( i + 1 in dom t1 implies t1 . (i + 1) = t2 . (i + 1) )
assume  i + 1 in dom t2 ; ::_thesis: i + 1 in dom t1
then  i + 1 <= len t2 by FINSEQ_3:25;
then  i < len t2 by NAT_1:13;
then  ( i in dom t2 & not emp t2 /. i ) by A24, A30, FINSEQ_3:25;
then  ( len t1 <> i & i <= len t1 ) by A19, A20, A28, FINSEQ_3:25, PARTFUN1:def_6;
then  i < len t1 by XXREAL_0:1;
then  ( 1 <= i + 1 & i + 1 <= len t1 ) by NAT_1:11, NAT_1:13;
hence  i + 1 in dom t1 by FINSEQ_3:25; ::_thesis: verum
end;
assume A32: i + 1 in dom t1 ; ::_thesis: t1 . (i + 1) = t2 . (i + 1)
then  ( i + 1 <= len t1 & i + 1 <= len t2 ) by A31, FINSEQ_3:25;
then  ( i < len t1 & i < len t2 ) by NAT_1:13;
then A33: ( i in dom t1 & t1 /. (i + 1) = pop (t1 /. i) & i in dom t2 & t2 /. (i + 1) = pop (t2 /. i) ) by A21, A24, A30, FINSEQ_3:25;
then  ( t1 /. i = t1 . i & t2 /. i = t2 . i & t1 /. (i + 1) = t1 . (i + 1) & t2 /. (i + 1) = t2 . (i + 1) ) by A32, A31, PARTFUN1:def_6;
hence  t1 . (i + 1) = t2 . (i + 1) by A28, A33; ::_thesis: verum
end;
end;
end;
A34: for i being Nat holds S1[i] from NAT_1:sch_2(A26, A27);
 dom t1 = dom t2
proof
thus  dom t1 c= dom t2 :: according to XBOOLE_0:def_10 ::_thesis: dom t2 c= dom t1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom t1 or x in dom t2 )
thus  ( not x in dom t1 or x in dom t2 ) by A34; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom t2 or x in dom t1 )
thus  ( not x in dom t2 or x in dom t1 ) by A34; ::_thesis: verum
end;
then  len t1 = len t2 by FINSEQ_3:29;
hence  x1 = x2 by A20, A23, A25, A34; ::_thesis: verum
end;
end;

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

theorem Th26: :: STACKS_1:26
for X being StackAlgebra
for s being stack of X st emp s holds
core s = s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st emp s holds
core s = s
let s be stack of X; ::_thesis: ( emp s implies core s = s )
set R = ConstructionRed X;
assume A1: emp s ; ::_thesis: core s = s
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A2: ( t . 1 = s & t . (len t) = core s ) and
A3: for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by Def19;
A4: 1 in dom t by FINSEQ_5:6;
then  t /. 1 = t . 1 by PARTFUN1:def_6;
then  ( 1 <= len t & len t <= 1 ) by A1, A2, A3, A4, FINSEQ_3:25;
hence  core s = s by A2, XXREAL_0:1; ::_thesis: verum
end;

theorem Th27: :: STACKS_1:27
for X being StackAlgebra
for s being stack of X
for e being Element of X holds core (push (e,s)) = core s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for e being Element of X holds core (push (e,s)) = core s
let s be stack of X; ::_thesis: for e being Element of X holds core (push (e,s)) = core s
let e be Element of X; ::_thesis: core (push (e,s)) = core s
set R = ConstructionRed X;
set A = the carrier' of X;
A1: emp core s by Def19;
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A2: ( t . 1 = s & t . (len t) = core s ) and
A3: for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by Def19;
 ( not emp push (e,s) & pop (push (e,s)) = s ) by Def11, Def12;
then  [(push (e,s)),s] in ConstructionRed X by Def18;
then reconsider u = <*(push (e,s)),s*> as RedSequence of ConstructionRed X by REWRITE1:7;
 ( u . 2 = s & len u = 2 ) by FINSEQ_1:44;
then reconsider v = u $^ t as RedSequence of ConstructionRed X by A2, REWRITE1:8;
A4: v = <*(push (e,s))*> ^ t by REWRITE1:2;
then A5: v . 1 = push (e,s) by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
A6: len <*(push (e,s))*> = 1 by FINSEQ_1:40;
then A7: len v = 1 + (len t) by A4, FINSEQ_1:22;
 len t in dom t by FINSEQ_5:6;
then A8: v . (len v) = t . (len t) by A4, A6, A7, FINSEQ_1:def_7;
now__::_thesis:_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; ::_thesis: ( 1 <= i & i < len v implies ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) ) )
assume A9: ( 1 <= i & i < len v ) ; ::_thesis: ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
 i in NAT by ORDINAL1:def_12;
then  ( i in dom v & i + 1 in dom v ) by A9, MSUALG_8:1;
then A10: ( v /. i = v . i & v /. (i + 1) = v . (i + 1) ) by PARTFUN1:def_6;
consider j being Nat such that
A11: i = 1 + j by A9, NAT_1:10;
A12: j < len t by A7, A9, A11, XREAL_1:6;
percases ( i = 1 or i > 1 ) by A9, XXREAL_0:1;
supposeA13: i = 1 ; ::_thesis: ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
hence  not emp v /. i by A5, A10, Def12; ::_thesis: v /. (i + 1) = pop (v /. i)
 1 in dom t by FINSEQ_5:6;
hence v /. (i + 1) = t . 1 by A4, A6, A10, A13, FINSEQ_1:def_7
.= pop (v /. i) by A13, A2, A5, A10, Def11 ;
::_thesis: verum
end;
suppose i > 1 ; ::_thesis: ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
then A14: ( j >= 1 & j in NAT ) by A11, NAT_1:13, ORDINAL1:def_12;
then  ( j in dom t & i in dom t ) by A11, A12, MSUALG_8:1;
then  ( t . j = v . i & t /. j = t . j & t . i = v . (i + 1) & t /. i = t . i ) by A4, A6, A11, FINSEQ_1:def_7, PARTFUN1:def_6;
hence  ( not emp v /. i & v /. (i + 1) = pop (v /. i) ) by A3, A10, A11, A12, A14; ::_thesis: verum
end;
end;
end;
hence  core (push (e,s)) = core s by A1, A2, A5, A8, Def19; ::_thesis: verum
end;

theorem Th28: :: STACKS_1:28
for X being StackAlgebra
for s being stack of X st not emp s holds
core (pop s) = core s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X st not emp s holds
core (pop s) = core s
let s be stack of X; ::_thesis: ( not emp s implies core (pop s) = core s )
set R = ConstructionRed X;
set A = the carrier' of X;
assume A1: not emp s ; ::_thesis: 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__::_thesis:_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; ::_thesis: ( 1 <= i & i < len v implies ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) ) )
assume A10: ( 1 <= i & i < len v ) ; ::_thesis: ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
 i in NAT by ORDINAL1:def_12;
then  ( 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;
percases ( i = 1 or i > 1 ) by A10, XXREAL_0:1;
supposeA14: i = 1 ; ::_thesis: ( not emp v /. b1 & v /. (b1 + 1) = pop (v /. b1) )
hence  not emp v /. i by A1, A5, A11, FINSEQ_1:41; ::_thesis: 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 ;
::_thesis: verum
end;
suppose i > 1 ; ::_thesis: ( 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; ::_thesis: verum
end;
end;
end;
hence  core (pop s) = core s by A2, A3, A6, A9, Def19; ::_thesis: verum
end;

theorem Th29: :: STACKS_1:29
for X being StackAlgebra
for s being stack of X holds core s in coset s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X holds core s in coset s
let s be stack of X; ::_thesis: core s in coset s
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A1: ( t . 1 = s & t . (len t) = core s ) and
 for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by Def19;
 ConstructionRed X reduces s, core s by A1, REWRITE1:def_3;
then  core s in  {  s1 where s1 is stack of X : ConstructionRed X reduces s,s1  }  ;
hence  core s in coset s by Th25; ::_thesis: verum
end;

theorem Th30: :: STACKS_1:30
for X being StackAlgebra
for s being stack of X
for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )
let s be stack of X; ::_thesis: for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )
set A = the carrier of X;
defpred S1[ FinSequence of the carrier of X] means  ex s1 being stack of X st
( |.s1.| = $1 & s1 in coset s );
 emp core s by Def19;
then  |.(core s).| = {} by Th5;
then A1: S1[ <*> the carrier of X] by Th29;
A2: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_X
for_x_being_Element_of_the_carrier_of_X_st_S1[p]_holds_
S1[<*x*>_^_p]
let p be FinSequence of the carrier of X; ::_thesis: for x being Element of the carrier of X st S1[p] holds
S1[<*x*> ^ p]
let x be Element of the carrier of X; ::_thesis: ( S1[p] implies S1[<*x*> ^ p] )
assume  S1[p] ; ::_thesis: S1[<*x*> ^ p]
then consider s1 being stack of X such that
A3: ( |.s1.| = p & s1 in coset s ) ;
thus  S1[<*x*> ^ p] ::_thesis: verum
proof
take s2 = push (x,s1); ::_thesis: ( |.s2.| = <*x*> ^ p & s2 in coset s )
thus  ( |.s2.| = <*x*> ^ p & s2 in coset s ) by A3, Th8, Def17; ::_thesis: verum
end;
end;
 for p being FinSequence of the carrier of X holds S1[p] from STACKS_1:sch_1(A1, A2);
hence  for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s ) ; ::_thesis: verum
end;

theorem Th31: :: STACKS_1:31
for X being StackAlgebra
for s1, s being stack of X st s1 in coset s holds
core s1 = core s
proof
let X be StackAlgebra; ::_thesis: for s1, s being stack of X st s1 in coset s holds
core s1 = core s
let s1, s be stack of X; ::_thesis: ( s1 in coset s implies core s1 = core s )
assume A1: s1 in coset s ; ::_thesis: core s1 = core s
set R = ConstructionRed X;
defpred S1[ stack of X] means  core $1 = core s;
A2: S1[s] ;
 coset s =  {  s2 where s2 is stack of X : ConstructionRed X reduces s,s2  }  by Th25;
then  ex s2 being stack of X st
( s1 = s2 & ConstructionRed X reduces s,s2 ) by A1;
then A3: ConstructionRed X reduces s,s1 ;
A4: now__::_thesis:_for_x,_y_being_stack_of_X_st_ConstructionRed_X_reduces_s,x_&_[x,y]_in_ConstructionRed_X_&_S1[x]_holds_
S1[y]
let x, y be stack of X; ::_thesis: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S1[x] implies S1[y] )
assume A5: ( ConstructionRed X reduces s,x & [x,y] in ConstructionRed X & S1[x] ) ; ::_thesis: S1[y]
then  ( ( not emp x & y = pop x ) or ex e being Element of X st y = push (e,x) ) by Def18;
hence  S1[y] by A5, Th27, Th28; ::_thesis: verum
end;
thus  S1[s1] from STACKS_1:sch_6(A2, A3, A4); ::_thesis: verum
end;

theorem Th32: :: STACKS_1:32
for X being StackAlgebra
for s1, s, s2 being stack of X st s1 in coset s & s2 in coset s & |.s1.| = |.s2.| holds
s1 = s2
proof
let X be StackAlgebra; ::_thesis: for s1, s, s2 being stack of X st s1 in coset s & s2 in coset s & |.s1.| = |.s2.| holds
s1 = s2
let s1, s, s2 be stack of X; ::_thesis: ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 )
defpred S1[ stack of X] means  for s2 being stack of X st $1 in coset s & s2 in coset s & |.$1.| = |.s2.| holds
$1 = s2;
A1: for s1 being stack of X st emp s1 holds
S1[s1]
proof
let s1 be stack of X; ::_thesis: ( emp s1 implies S1[s1] )
assume A2: emp s1 ; ::_thesis: S1[s1]
then A3: |.s1.| = {} by Th5;
let s2 be stack of X; ::_thesis: ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 )
assume  ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| ) ; ::_thesis: s1 = s2
then  ( core s1 = core s & core s2 = core s & emp s2 ) by A3, Th10, Th31;
then  ( core s = s1 & core s = s2 ) by A2, Th26;
hence  s1 = s2 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_s1_being_stack_of_X
for_e_being_Element_of_X_st_S1[s1]_holds_
S1[_push_(e,s1)]
let s1 be stack of X; ::_thesis: for e being Element of X st S1[s1] holds
S1[ push (e,s1)]
let e be Element of X; ::_thesis: ( S1[s1] implies S1[ push (e,s1)] )
assume A5: S1[s1] ; ::_thesis: S1[ push (e,s1)]
thus  S1[ push (e,s1)] ::_thesis: verum
proof
let s2 be stack of X; ::_thesis: ( push (e,s1) in coset s & s2 in coset s & |.(push (e,s1)).| = |.s2.| implies push (e,s1) = s2 )
assume A6: ( push (e,s1) in coset s & s2 in coset s & |.(push (e,s1)).| = |.s2.| ) ; ::_thesis: push (e,s1) = s2
then A7: |.s2.| = <*e*> ^ |.s1.| by Th8;
then  not emp s2 by Th5;
then A8: s2 = push ((top s2),(pop s2)) by Def9;
then A9: ( s1 in coset s & pop s2 in coset s ) by A6, Th20;
 |.s2.| = <*(top s2)*> ^ |.(pop s2).| by A8, Th8;
then  ( e = |.s2.| . 1 & |.s2.| . 1 = top s2 & |.s1.| = |.(pop s2).| ) by A7, FINSEQ_1:41, HILBERT2:2;
hence  push (e,s1) = s2 by A5, A8, A9; ::_thesis: verum
end;
end;
 S1[s1] from STACKS_1:sch_3(A1, A4);
hence  ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 ) ; ::_thesis: verum
end;

theorem Th33: :: STACKS_1:33
for X being StackAlgebra
for s1, s2 being stack of X ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}
proof
let X be StackAlgebra; ::_thesis: for s1, s2 being stack of X ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}
let s1, s2 be stack of X; ::_thesis: ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}
consider s being stack of X such that
A1: ( |.s.| = |.s2.| & s in coset s1 ) by Th30;
take  s ; ::_thesis: (coset s1) /\ (Class ((==_ X),s2)) = {s}
thus  (coset s1) /\ (Class ((==_ X),s2)) c= {s} :: according to XBOOLE_0:def_10 ::_thesis: {s} c= (coset s1) /\ (Class ((==_ X),s2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (coset s1) /\ (Class ((==_ X),s2)) or x in {s} )
assume A2: x in (coset s1) /\ (Class ((==_ X),s2)) ; ::_thesis: x in {s}
then A3: ( x in coset s1 & x in Class ((==_ X),s2) ) by XBOOLE_0:def_4;
reconsider x = x as stack of X by A2;
 [s2,x] in ==_ X by A3, EQREL_1:18;
then  s2 == x by Def16;
then  |.s2.| = |.x.| by Def14;
then  s = x by A1, A3, Th32;
hence  x in {s} by TARSKI:def_1; ::_thesis: verum
end;
 s == s2 by A1, Def14;
then  [s2,s] in ==_ X by Def16;
then  s in Class ((==_ X),s2) by EQREL_1:18;
then  ( {s} c= Class ((==_ X),s2) & {s} c= coset s1 ) by A1, ZFMISC_1:31;
hence  {s} c= (coset s1) /\ (Class ((==_ X),s2)) by XBOOLE_1:19; ::_thesis: verum
end;

begin

definition
let X be StackAlgebra;
funcX /==  ->  strict StackSystem  means :Def20: :: STACKS_1:def 20
( the carrier of it = the carrier of X & the carrier' of it = Class (==_ X) & the s_empty of it = { the s_empty of X} & the s_push of it = the s_push of X /\/ (==_ X) & the s_pop of it = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of it = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) );
uniqueness
 for b1, b2 being strict StackSystem st the carrier of b1 = the carrier of X & the carrier' of b1 = Class (==_ X) & the s_empty of b1 = { the s_empty of X} & the s_push of b1 = the s_push of X /\/ (==_ X) & the s_pop of b1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of b1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) & the carrier of b2 = the carrier of X & the carrier' of b2 = Class (==_ X) & the s_empty of b2 = { the s_empty of X} & the s_push of b2 = the s_push of X /\/ (==_ X) & the s_pop of b2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of b2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) holds
b1 = b2
proof
let X1, X2 be strict StackSystem ; ::_thesis: ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) & the carrier of X2 = the carrier of X & the carrier' of X2 = Class (==_ X) & the s_empty of X2 = { the s_empty of X} & the s_push of X2 = the s_push of X /\/ (==_ X) & the s_pop of X2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of X2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) implies X1 = X2 )
assume that
A1: ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) ) and
A2: for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) and
A3: ( the carrier of X2 = the carrier of X & the carrier' of X2 = Class (==_ X) & the s_empty of X2 = { the s_empty of X} & the s_push of X2 = the s_push of X /\/ (==_ X) & the s_pop of X2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) ) and
A4: for f being Choice_Function of Class (==_ X) holds the s_top of X2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ; ::_thesis: X1 = X2
set f = the Choice_Function of Class (==_ X);
 ( the s_top of X1 = ( the s_top of X * the Choice_Function of Class (==_ X)) +* ( the s_empty of X, the Element of the carrier of X) & the s_top of X2 = ( the s_top of X * the Choice_Function of Class (==_ X)) +* ( the s_empty of X, the Element of the carrier of X) ) by A2, A4;
hence  X1 = X2 by A1, A3; ::_thesis: verum
end;
existence
 ex b1 being strict StackSystem st
( the carrier of b1 = the carrier of X & the carrier' of b1 = Class (==_ X) & the s_empty of b1 = { the s_empty of X} & the s_push of b1 = the s_push of X /\/ (==_ X) & the s_pop of b1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of b1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) )
proof
set f = the Choice_Function of Class (==_ X);
A5: union (Class (==_ X)) = the carrier' of X by EQREL_1:def_4;
then reconsider f = the Choice_Function of Class (==_ X) as Function of (Class (==_ X)), the carrier' of X ;
consider s being stack of X such that
A6: emp s by Th2;
A7: Class ((==_ X),s) = the s_empty of X by A6, Th19;
reconsider E = Class ((==_ X),s) as Element of Class (==_ X) by EQREL_1:def_3;
set g = the s_top of X * f;
take X1 = StackSystem(# the carrier of X,(Class (==_ X)),{E},( the s_push of X /\/ (==_ X)),(( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X)),(( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) #); ::_thesis: ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) )
thus  ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) ) by A6, Th19; ::_thesis: for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)
let h be Choice_Function of Class (==_ X); ::_thesis: the s_top of X1 = ( the s_top of X * h) +* ( the s_empty of X, the Element of the carrier of X)
reconsider h0 = h as Function of (Class (==_ X)), the carrier' of X by A5;
now__::_thesis:_for_a_being_Element_of_Class_(==__X)_holds_((_the_s_top_of_X_*_f)_+*_(_the_s_empty_of_X,_the_Element_of_the_carrier_of_X))_._a_=_((_the_s_top_of_X_*_h0)_+*_(_the_s_empty_of_X,_the_Element_of_the_carrier_of_X))_._a
let a be Element of Class (==_ X); ::_thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b1 = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b1
consider s1 being stack of X such that
A8: a = Class ((==_ X),s1) by EQREL_1:36;
percases ( emp s1 or not emp s1 ) ;
suppose emp s1 ; ::_thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b1 = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b1
then  ( s1 in the s_empty of X & dom ( the s_top of X * f) = Class (==_ X) & dom ( the s_top of X * h0) = Class (==_ X) ) by Def3, FUNCT_2:def_1;
then A9: ( a = E & E in dom ( the s_top of X * f) & E in dom ( the s_top of X * h0) ) by A7, A8, EQREL_1:23;
then  (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = the Element of the carrier of X by A7, FUNCT_7:31;
hence  (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . a by A7, A9, FUNCT_7:31; ::_thesis: verum
end;
supposeA10: not emp s1 ; ::_thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b1 = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b1
then  s1 nin E by A7, Def3;
then A11: a <> E by A8, EQREL_1:23;
 {} nin Class (==_ X) by SETFAM_1:def_8;
then  ( f . a in a & h . a in a ) by ORDERS_1:def_1;
then  ( [s1,(f . a)] in ==_ X & [s1,(h . a)] in ==_ X ) by A8, EQREL_1:18;
then  ( s1 == f . a & s1 == h0 . a ) by Def16;
then  ( f . a == h0 . a & not emp f . a ) by A10, Th13, Th14;
then  top (f . a) = top (h0 . a) by Th18;
then  ( the s_top of X * f) . a = top (h0 . a) by FUNCT_2:15;
then  ( the s_top of X * f) . a = ( the s_top of X * h0) . a by FUNCT_2:15;
then  (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = ( the s_top of X * h0) . a by A7, A11, FUNCT_7:32;
hence  (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . a by A7, A11, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence  the s_top of X1 = ( the s_top of X * h) +* ( the s_empty of X, the Element of the carrier of X) by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines /== STACKS_1:def_20_:_
 for X being StackAlgebra
for b2 being strict StackSystem holds
( b2 = X /== iff ( the carrier of b2 = the carrier of X & the carrier' of b2 = Class (==_ X) & the s_empty of b2 = { the s_empty of X} & the s_push of b2 = the s_push of X /\/ (==_ X) & the s_pop of b2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of b2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) ) );

registration
let X be StackAlgebra;
clusterX /==  ->  non empty non void strict ;
coherence
 ( not X /== is empty & not X /== is void )
proof
 ( the carrier of (X /==) = the carrier of X & the carrier' of (X /==) = Class (==_ X) ) by Def20;
hence  ( not X /== is empty & not X /== is void ) ; ::_thesis: verum
end;
end;

theorem Th34: :: STACKS_1:34
for X being StackAlgebra
for S being stack of (X /==) ex s being stack of X st S = Class ((==_ X),s)
proof
let X be StackAlgebra; ::_thesis: for S being stack of (X /==) ex s being stack of X st S = Class ((==_ X),s)
let S be stack of (X /==); ::_thesis: ex s being stack of X st S = Class ((==_ X),s)
 the carrier' of (X /==) = Class (==_ X) by Def20;
then  S in Class (==_ X) ;
then  ex x being set st
( x in the carrier' of X & S = Class ((==_ X),x) ) by EQREL_1:def_3;
hence  ex s being stack of X st S = Class ((==_ X),s) ; ::_thesis: verum
end;

theorem Th35: :: STACKS_1:35
for X being StackAlgebra
for s being stack of X holds Class ((==_ X),s) is stack of (X /==)
proof
let X be StackAlgebra; ::_thesis: for s being stack of X holds Class ((==_ X),s) is stack of (X /==)
let s be stack of X; ::_thesis: Class ((==_ X),s) is stack of (X /==)
 the carrier' of (X /==) = Class (==_ X) by Def20;
hence  Class ((==_ X),s) is stack of (X /==) by EQREL_1:def_3; ::_thesis: verum
end;

theorem Th36: :: STACKS_1:36
for X being StackAlgebra
for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
let s be stack of X; ::_thesis: for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
let S be stack of (X /==); ::_thesis: ( S = Class ((==_ X),s) implies ( emp s iff emp S ) )
assume A1: S = Class ((==_ X),s) ; ::_thesis: ( emp s iff emp S )
consider s1 being stack of X such that
A2: emp s1 by Th2;
 ( emp S iff S in the s_empty of (X /==) ) by Def3;
then  ( emp S iff S in { the s_empty of X} ) by Def20;
then  ( emp S iff S = the s_empty of X ) by TARSKI:def_1;
then  ( emp S iff S = Class ((==_ X),s1) ) by A2, Th19;
then  ( emp S iff [s,s1] in ==_ X ) by A1, EQREL_1:35;
then  ( emp S iff s == s1 ) by Def16;
hence  ( emp s iff emp S ) by A2, Th14, Th15; ::_thesis: verum
end;

theorem Th37: :: STACKS_1:37
for X being StackAlgebra
for S being stack of (X /==) holds
( emp S iff S = the s_empty of X )
proof
let X be StackAlgebra; ::_thesis: for S being stack of (X /==) holds
( emp S iff S = the s_empty of X )
let S be stack of (X /==); ::_thesis: ( emp S iff S = the s_empty of X )
 the carrier' of (X /==) = Class (==_ X) by Def20;
then  S in Class (==_ X) ;
then consider x being set  such that
A1: ( x in the carrier' of X & S = Class ((==_ X),x) ) by EQREL_1:def_3;
reconsider x = x as stack of X by A1;
hereby  ::_thesis: ( S = the s_empty of X implies emp S )
assume  emp S ; ::_thesis: S = the s_empty of X
then  emp x by A1, Th36;
hence  S = the s_empty of X by A1, Th19; ::_thesis: verum
end;
assume  S = the s_empty of X ; ::_thesis: emp S
then  x in the s_empty of X by A1, EQREL_1:20;
then  emp x by Def3;
hence  emp S by A1, Th36; ::_thesis: verum
end;

theorem Th38: :: STACKS_1:38
for X being StackAlgebra
for s being stack of X
for e being Element of X
for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for e being Element of X
for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let s be stack of X; ::_thesis: for e being Element of X
for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let e be Element of X; ::_thesis: for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let S be stack of (X /==); ::_thesis: for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let E be Element of (X /==); ::_thesis: ( S = Class ((==_ X),s) & E = e implies ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) )
assume A1: S = Class ((==_ X),s) ; ::_thesis: ( not E = e or ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) )
assume A2: E = e ; ::_thesis: ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
A3: s in S by A1, EQREL_1:20;
A4: S in Class (==_ X) by A1, EQREL_1:def_3;
A5: the s_push of X is BinOp of the carrier of X, the carrier' of X, ==_ X
proof
let x be Element of X; :: according to STACKS_1:def_1 ::_thesis: for y1, y2 being Element of the carrier' of X st [y1,y2] in ==_ X holds
[( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X
let y1, y2 be stack of X; ::_thesis: ( [y1,y2] in ==_ X implies [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X )
assume  [y1,y2] in ==_ X ; ::_thesis: [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X
then  y1 == y2 by Def16;
then  push (x,y1) == push (x,y2) by Th16;
hence  [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X by Def16; ::_thesis: verum
end;
push (E,S) = ( the s_push of X /\/ (==_ X)) . (E,S) by Def20
.= Class ((==_ X),(push (e,s))) by A2, A3, A4, A5, Def2 ;
hence  ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) by EQREL_1:20; ::_thesis: verum
end;

theorem Th39: :: STACKS_1:39
for X being StackAlgebra
for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
let s be stack of X; ::_thesis: for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
set p = the s_pop of X;
set i = id the s_empty of X;
let S be stack of (X /==); ::_thesis: ( S = Class ((==_ X),s) & not emp s implies ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume A1: S = Class ((==_ X),s) ; ::_thesis: ( emp s or ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume A2: not emp s ; ::_thesis: ( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
A3: s in S by A1, EQREL_1:20;
A4: S in Class (==_ X) by A1, EQREL_1:def_3;
A5: dom (id the s_empty of X) = the s_empty of X ;
A6: the s_pop of X +* (id the s_empty of X) is UnOp of the carrier' of X, ==_ X
proof
let y1, y2 be stack of X; :: according to FILTER_1:def_1 ::_thesis: ( not [y1,y2] in ==_ X or [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X )
assume A7: [y1,y2] in ==_ X ; ::_thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X
then A8: y1 == y2 by Def16;
percases ( not emp y1 or emp y1 ) ;
supposeA9: not emp y1 ; ::_thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X
then  not emp y2 by A8, Th14;
then  ( y1 nin the s_empty of X & y2 nin the s_empty of X ) by A9, Def3;
then A10: ( ( the s_pop of X +* (id the s_empty of X)) . y1 = the s_pop of X . y1 & ( the s_pop of X +* (id the s_empty of X)) . y2 = the s_pop of X . y2 ) by A5, FUNCT_4:11;
 pop y1 == pop y2 by A8, A9, Th17;
hence  [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X by A10, Def16; ::_thesis: verum
end;
supposeA11: emp y1 ; ::_thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X
then  emp y2 by A8, Th14;
then  ( y1 in the s_empty of X & y2 in the s_empty of X ) by A11, Def3;
then  ( ( the s_pop of X +* (id the s_empty of X)) . y1 = (id the s_empty of X) . y1 & (id the s_empty of X) . y1 = y1 & ( the s_pop of X +* (id the s_empty of X)) . y2 = (id the s_empty of X) . y2 & (id the s_empty of X) . y2 = y2 ) by A5, FUNCT_1:18, FUNCT_4:13;
hence  [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X by A7; ::_thesis: verum
end;
end;
end;
A12: s nin the s_empty of X by A2, Def3;
pop S = (( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X)) . S by Def20
.= Class ((==_ X),(( the s_pop of X +* (id the s_empty of X)) . s)) by A3, A4, A6, FILTER_1:def_3
.= Class ((==_ X),(pop s)) by A5, A12, FUNCT_4:11 ;
hence  ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) by EQREL_1:20; ::_thesis: verum
end;

theorem Th40: :: STACKS_1:40
for X being StackAlgebra
for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
let s be stack of X; ::_thesis: for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
set t = the s_top of X;
set A = the s_empty of X;
set e = the Element of the carrier of X;
let S be stack of (X /==); ::_thesis: ( S = Class ((==_ X),s) & not emp s implies top S = top s )
assume A1: S = Class ((==_ X),s) ; ::_thesis: ( emp s or top S = top s )
assume A2: not emp s ; ::_thesis: top S = top s
then  not emp S by A1, Th36;
then A3: S <> the s_empty of X by Th37;
set f = the Choice_Function of Class (==_ X);
A4: ( S in Class (==_ X) & {} nin Class (==_ X) ) by A1, EQREL_1:def_3, SETFAM_1:def_8;
then A5: the Choice_Function of Class (==_ X) . S in S by ORDERS_1:def_1;
then reconsider x = the Choice_Function of Class (==_ X) . S as stack of X by A1;
 [s,x] in ==_ X by A1, A5, EQREL_1:18;
then A6: s == x by Def16;
A7: dom the Choice_Function of Class (==_ X) = Class (==_ X) by A4, RLVECT_3:28;
 the s_top of (X /==) = ( the s_top of X * the Choice_Function of Class (==_ X)) +* ( the s_empty of X, the Element of the carrier of X) by Def20;
hence  top S = ( the s_top of X * the Choice_Function of Class (==_ X)) . S by A3, FUNCT_7:32
.= top x by A4, A7, FUNCT_1:13
.= top s by A6, A2, Th18 ;
::_thesis: verum
end;

registration
let X be StackAlgebra;
clusterX /==  ->  strict pop-finite ;
coherence
 X /== is pop-finite
proof
let f be Function of NAT, the carrier' of (X /==); :: according to STACKS_1:def_8 ::_thesis: ex i being Nat ex s being stack of (X /==) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
set s1 = the stack of X;
defpred S1[ set , set ] means c2 in (coset the stack of X) /\ X;
A1: for x being set st x in Class (==_ X) holds
ex y being set st
( y in the carrier' of X & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Class (==_ X) implies ex y being set st
( y in the carrier' of X & S1[x,y] ) )
assume  x in Class (==_ X) ; ::_thesis: ex y being set st
( y in the carrier' of X & S1[x,y] )
then consider s2 being stack of X such that
A2: x = Class ((==_ X),s2) by EQREL_1:36;
consider s being stack of X such that
A3: (coset the stack of X) /\ (Class ((==_ X),s2)) = {s} by Th33;
take  s ; ::_thesis: ( s in the carrier' of X & S1[x,s] )
thus  s in the carrier' of X ; ::_thesis: S1[x,s]
thus  s in (coset the stack of X) /\ x by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
consider g being Function such that
A4: ( dom g = Class (==_ X) & rng g c= the carrier' of X & ( for x being set st x in Class (==_ X) holds
S1[x,g . x] ) ) from FUNCT_1:sch_5(A1);
A5: the carrier' of (X /==) = Class (==_ X) by Def20;
then reconsider g = g as Function of the carrier' of (X /==), the carrier' of X by A4, FUNCT_2:2;
consider i being Nat, s being stack of X such that
A6: ( (g * f) . i = s & ( not emp s implies (g * f) . (i + 1) <> pop s ) ) by Def8;
reconsider S = Class ((==_ X),s) as stack of (X /==) by A5, EQREL_1:def_3;
take  i ; ::_thesis: ex s being stack of (X /==) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
take  S ; ::_thesis: ( f . i = S & ( not emp S implies f . (i + 1) <> pop S ) )
consider s2 being stack of X such that
A7: f . i = Class ((==_ X),s2) by A5, EQREL_1:36;
 i in NAT by ORDINAL1:def_12;
then  s = g . (f . i) by A6, FUNCT_2:15;
then  s in (coset the stack of X) /\ (f . i) by A4, A5;
then A8: ( s in coset the stack of X & s in f . i ) by XBOOLE_0:def_4;
hence  f . i = S by A7, EQREL_1:23; ::_thesis: ( not emp S implies f . (i + 1) <> pop S )
assume A9: not emp S ; ::_thesis: f . (i + 1) <> pop S
then A10: not emp s by Th36;
assume A11: f . (i + 1) = pop S ; ::_thesis: contradiction
then A12: f . (i + 1) = Class ((==_ X),(pop s)) by A10, Th39;
set s3 = g . (f . (i + 1));
consider s4 being stack of X such that
A13: (coset the stack of X) /\ (f . (i + 1)) = {s4} by A12, Th33;
 ( pop s in coset the stack of X & pop s in pop S & pop S = f . (i + 1) ) by A8, A11, A10, Def17, Th39;
then A14: pop s in {s4} by A13, XBOOLE_0:def_4;
 g . (f . (i + 1)) in (coset the stack of X) /\ (f . (i + 1)) by A4, A5;
then  ( g . (f . (i + 1)) = s4 & pop s = s4 ) by A13, A14, TARSKI:def_1;
hence  contradiction by A6, A9, Th36, FUNCT_2:15; ::_thesis: verum
end;
clusterX /==  ->  strict push-pop ;
coherence
 X /== is push-pop
proof
let S be stack of (X /==); :: according to STACKS_1:def_9 ::_thesis: ( not emp S implies S = push ((top S),(pop S)) )
consider s being stack of X such that
A15: S = Class ((==_ X),s) by Th34;
assume  not emp S ; ::_thesis: S = push ((top S),(pop S))
then A16: not emp s by A15, Th36;
reconsider P = Class ((==_ X),(pop s)) as stack of (X /==) by Th35;
reconsider E = top s as Element of (X /==) by Def20;
thus S = Class ((==_ X),(push ((top s),(pop s)))) by A15, A16, Def9
.= push (E,P) by Th38
.= push ((top S),P) by A15, A16, Th40
.= push ((top S),(pop S)) by A15, A16, Th39 ; ::_thesis: verum
end;
clusterX /==  ->  strict top-push ;
coherence
 X /== is top-push
proof
let S be stack of (X /==); :: according to STACKS_1:def_10 ::_thesis: for e being Element of (X /==) holds e = top (push (e,S))
let E be Element of (X /==); ::_thesis: E = top (push (E,S))
consider s being stack of X such that
A17: S = Class ((==_ X),s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class ((==_ X),(push (e,s))) as stack of (X /==) by Th35;
A18: not emp push (e,s) by Def12;
thus E = top (push (e,s)) by Def10
.= top P by A18, Th40
.= top (push (E,S)) by A17, Th38 ; ::_thesis: verum
end;
clusterX /==  ->  strict pop-push ;
coherence
 X /== is pop-push
proof
let S be stack of (X /==); :: according to STACKS_1:def_11 ::_thesis: for e being Element of (X /==) holds S = pop (push (e,S))
let E be Element of (X /==); ::_thesis: S = pop (push (E,S))
consider s being stack of X such that
A19: S = Class ((==_ X),s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class ((==_ X),(push (e,s))) as stack of (X /==) by Th35;
A20: not emp push (e,s) by Def12;
thus S = Class ((==_ X),(pop (push (e,s)))) by A19, Def11
.= pop P by A20, Th39
.= pop (push (E,S)) by A19, Th38 ; ::_thesis: verum
end;
clusterX /==  ->  strict push-non-empty ;
coherence
 X /== is push-non-empty
proof
let S be stack of (X /==); :: according to STACKS_1:def_12 ::_thesis: for e being Element of (X /==) holds not emp push (e,S)
let E be Element of (X /==); ::_thesis: not emp push (E,S)
consider s being stack of X such that
A21: S = Class ((==_ X),s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class ((==_ X),(push (e,s))) as stack of (X /==) by Th35;
 not emp push (e,s) by Def12;
then  not emp P by Th36;
hence  not emp push (E,S) by A21, Th38; ::_thesis: verum
end;
end;

theorem Th41: :: STACKS_1:41
for X being StackAlgebra
for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
proof
let X be StackAlgebra; ::_thesis: for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
let s be stack of X; ::_thesis: for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
defpred S1[ stack of X] means  for S being stack of (X /==) st S = Class ((==_ X),$1) holds
|.S.| = |.$1.|;
A1: for s1 being stack of X st emp s1 holds
S1[s1]
proof
let s1 be stack of X; ::_thesis: ( emp s1 implies S1[s1] )
assume A2: emp s1 ; ::_thesis: S1[s1]
let S be stack of (X /==); ::_thesis: ( S = Class ((==_ X),s1) implies |.S.| = |.s1.| )
assume  S = Class ((==_ X),s1) ; ::_thesis: |.S.| = |.s1.|
then  emp S by A2, Th36;
then  |.S.| = {} by Th5;
hence  |.S.| = |.s1.| by A2, Th5; ::_thesis: verum
end;
A3: for s1 being stack of X
for e being Element of X st S1[s1] holds
S1[ push (e,s1)]
proof
let s1 be stack of X; ::_thesis: for e being Element of X st S1[s1] holds
S1[ push (e,s1)]
let e be Element of X; ::_thesis: ( S1[s1] implies S1[ push (e,s1)] )
assume A4: S1[s1] ; ::_thesis: S1[ push (e,s1)]
reconsider E = e as Element of (X /==) by Def20;
let S be stack of (X /==); ::_thesis: ( S = Class ((==_ X),(push (e,s1))) implies |.S.| = |.(push (e,s1)).| )
assume A5: S = Class ((==_ X),(push (e,s1))) ; ::_thesis: |.S.| = |.(push (e,s1)).|
reconsider P = Class ((==_ X),s1) as stack of (X /==) by Th35;
 S = push (E,P) by A5, Th38;
hence |.S.| = <*E*> ^ |.P.| by Th8
.= <*e*> ^ |.s1.| by A4
.= |.(push (e,s1)).| by Th8 ;
::_thesis: verum
end;
thus  S1[s] from STACKS_1:sch_3(A1, A3); ::_thesis: verum
end;

registration
let X be StackAlgebra;
clusterX /==  ->  strict proper-for-identity ;
coherence
 X /== is proper-for-identity
proof
let S1, S2 be stack of (X /==); :: according to STACKS_1:def_15 ::_thesis: ( S1 == S2 implies S1 = S2 )
consider s1 being stack of X such that
A1: S1 = Class ((==_ X),s1) by Th34;
consider s2 being stack of X such that
A2: S2 = Class ((==_ X),s2) by Th34;
assume  |.S1.| = |.S2.| ; :: according to STACKS_1:def_14 ::_thesis: S1 = S2
then |.s1.| = |.S2.| by A1, Th41
.= |.s2.| by A2, Th41 ;
then  s1 == s2 by Def14;
then  [s1,s2] in ==_ X by Def16;
then  s2 in S1 by A1, EQREL_1:18;
hence  S1 = S2 by A1, A2, EQREL_1:23; ::_thesis: verum
end;
end;

registration
cluster non empty non void V67() pop-finite push-pop top-push pop-push push-non-empty proper-for-identity for StackSystem ;
existence
 ex b1 being StackAlgebra st b1 is proper-for-identity
proof
take  the StackAlgebra /== ; ::_thesis: the StackAlgebra /== is proper-for-identity
thus  the StackAlgebra /== is proper-for-identity ; ::_thesis: verum
end;
end;

begin

definition
let X1, X2 be StackAlgebra;
let F, G be Function;
predF,G form_isomorphism_between X1,X2 means :Def21: :: STACKS_1:def 21
( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one & dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one & ( for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = F . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) );
end;

:: deftheorem Def21 defines form_isomorphism_between STACKS_1:def_21_:_
 for X1, X2 being StackAlgebra
for F, G being Function holds
( F,G form_isomorphism_between X1,X2 iff ( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one & dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one & ( for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = F . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) ) );


theorem Th42: :: STACKS_1:42
for X being StackAlgebra holds id the carrier of X, id the carrier' of X form_isomorphism_between X,X
proof
let X be StackAlgebra; ::_thesis: id the carrier of X, id the carrier' of X form_isomorphism_between X,X
set F = id the carrier of X;
set G = id the carrier' of X;
thus  ( dom (id the carrier of X) = the carrier of X & rng (id the carrier of X) = the carrier of X & id the carrier of X is one-to-one ) ; :: according to STACKS_1:def_21 ::_thesis: ( dom (id the carrier' of X) = the carrier' of X & rng (id the carrier' of X) = the carrier' of X & id the carrier' of X is one-to-one & ( for s1, s2 being stack of X st s2 = (id the carrier' of X) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) ) ) )
thus  ( dom (id the carrier' of X) = the carrier' of X & rng (id the carrier' of X) = the carrier' of X & id the carrier' of X is one-to-one ) ; ::_thesis: for s1, s2 being stack of X st s2 = (id the carrier' of X) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) )
let s1, s2 be stack of X; ::_thesis: ( s2 = (id the carrier' of X) . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) ) )
assume A1: s2 = (id the carrier' of X) . s1 ; ::_thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) )
then A2: s2 = s1 by FUNCT_1:17;
thus  ( emp s1 iff emp s2 ) by A1, FUNCT_1:17; ::_thesis: ( not emp s1 iff ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) )
thus  ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) by A2, FUNCT_1:17; ::_thesis: for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1))
let e1, e2 be Element of X; ::_thesis: ( e2 = (id the carrier of X) . e1 implies push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) )
assume  e2 = (id the carrier of X) . e1 ; ::_thesis: push (e2,s2) = (id the carrier' of X) . (push (e1,s1))
then  e2 = e1 by FUNCT_1:17;
hence  push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) by A2, FUNCT_1:17; ::_thesis: verum
end;

theorem Th43: :: STACKS_1:43
for X1, X2 being StackAlgebra
for F, G being Function st F,G form_isomorphism_between X1,X2 holds
F " ,G " form_isomorphism_between X2,X1
proof
let X1, X2 be StackAlgebra; ::_thesis: for F, G being Function st F,G form_isomorphism_between X1,X2 holds
F " ,G " form_isomorphism_between X2,X1
let F, G be Function; ::_thesis: ( F,G form_isomorphism_between X1,X2 implies F " ,G " form_isomorphism_between X2,X1 )
assume that
A1: ( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one ) and
A2: ( dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one ) and
A3: for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = F . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ; :: according to STACKS_1:def_21 ::_thesis: F " ,G " form_isomorphism_between X2,X1
thus  ( dom (F ") = the carrier of X2 & rng (F ") = the carrier of X1 & F " is one-to-one ) by A1, FUNCT_1:33; :: according to STACKS_1:def_21 ::_thesis: ( dom (G ") = the carrier' of X2 & rng (G ") = the carrier' of X1 & G " is one-to-one & ( for s1 being stack of X2
for s2 being stack of X1 st s2 = (G ") . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) ) ) )
thus  ( dom (G ") = the carrier' of X2 & rng (G ") = the carrier' of X1 & G " is one-to-one ) by A2, FUNCT_1:33; ::_thesis: for s1 being stack of X2
for s2 being stack of X1 st s2 = (G ") . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
let s1 be stack of X2; ::_thesis: for s2 being stack of X1 st s2 = (G ") . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
let s2 be stack of X1; ::_thesis: ( s2 = (G ") . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) ) )
assume  s2 = (G ") . s1 ; ::_thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
then A4: G . s2 = s1 by A2, FUNCT_1:35;
hence A5: ( emp s1 iff emp s2 ) by A3; ::_thesis: ( not emp s1 iff ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) )
hereby  ::_thesis: for e1 being Element of X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1))
assume  not emp s1 ; ::_thesis: ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) )
then  ( pop s1 = G . (pop s2) & top s1 = F . (top s2) ) by A3, A5, A4;
hence  ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) by A1, A2, FUNCT_1:34; ::_thesis: verum
end;
let e1 be Element of X2; ::_thesis: for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1))
let e2 be Element of X1; ::_thesis: ( e2 = (F ") . e1 implies push (e2,s2) = (G ") . (push (e1,s1)) )
assume  e2 = (F ") . e1 ; ::_thesis: push (e2,s2) = (G ") . (push (e1,s1))
then  F . e2 = e1 by A1, FUNCT_1:35;
then  G . (push (e2,s2)) = push (e1,s1) by A3, A4;
hence  push (e2,s2) = (G ") . (push (e1,s1)) by A2, FUNCT_1:34; ::_thesis: verum
end;

theorem Th44: :: STACKS_1:44
for X1, X2, X3 being StackAlgebra
for F1, G1, F2, G2 being Function st F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 holds
F2 * F1,G2 * G1 form_isomorphism_between X1,X3
proof
let X1, X2, X3 be StackAlgebra; ::_thesis: for F1, G1, F2, G2 being Function st F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 holds
F2 * F1,G2 * G1 form_isomorphism_between X1,X3
let F1, G1, F2, G2 be Function; ::_thesis: ( F1,G1 form_isomorphism_between X1,X2 & F2,G2 form_isomorphism_between X2,X3 implies F2 * F1,G2 * G1 form_isomorphism_between X1,X3 )
assume that
A1: ( dom F1 = the carrier of X1 & rng F1 = the carrier of X2 & F1 is one-to-one ) and
A2: ( dom G1 = the carrier' of X1 & rng G1 = the carrier' of X2 & G1 is one-to-one ) and
A3: for s1 being stack of X1
for s2 being stack of X2 st s2 = G1 . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G1 . (pop s1) & top s2 = F1 . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F1 . e1 holds
push (e2,s2) = G1 . (push (e1,s1)) ) ) and
A4: ( dom F2 = the carrier of X2 & rng F2 = the carrier of X3 & F2 is one-to-one ) and
A5: ( dom G2 = the carrier' of X2 & rng G2 = the carrier' of X3 & G2 is one-to-one ) and
A6: for s1 being stack of X2
for s2 being stack of X3 st s2 = G2 . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G2 . (pop s1) & top s2 = F2 . (top s1) ) ) & ( for e1 being Element of X2
for e2 being Element of X3 st e2 = F2 . e1 holds
push (e2,s2) = G2 . (push (e1,s1)) ) ) ; :: according to STACKS_1:def_21 ::_thesis: F2 * F1,G2 * G1 form_isomorphism_between X1,X3
thus  ( dom (F2 * F1) = the carrier of X1 & rng (F2 * F1) = the carrier of X3 & F2 * F1 is one-to-one ) by A1, A4, RELAT_1:27, RELAT_1:28; :: according to STACKS_1:def_21 ::_thesis: ( dom (G2 * G1) = the carrier' of X1 & rng (G2 * G1) = the carrier' of X3 & G2 * G1 is one-to-one & ( for s1 being stack of X1
for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) ) ) )
thus  ( dom (G2 * G1) = the carrier' of X1 & rng (G2 * G1) = the carrier' of X3 & G2 * G1 is one-to-one ) by A2, A5, RELAT_1:27, RELAT_1:28; ::_thesis: for s1 being stack of X1
for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
let s1 be stack of X1; ::_thesis: for s2 being stack of X3 st s2 = (G2 * G1) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
let s2 be stack of X3; ::_thesis: ( s2 = (G2 * G1) . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) ) )
reconsider s3 = G1 . s1 as stack of X2 by A2, FUNCT_1:def_3;
assume  s2 = (G2 * G1) . s1 ; ::_thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1)) ) )
then A7: s2 = G2 . s3 by A2, FUNCT_1:13;
 ( emp s1 iff emp s3 ) by A3;
hence  ( emp s1 iff emp s2 ) by A6, A7; ::_thesis: ( not emp s1 iff ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) )
hereby  ::_thesis: for e1 being Element of X1
for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1))
assume  not emp s1 ; ::_thesis: ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) )
then  ( pop s3 = G1 . (pop s1) & top s3 = F1 . (top s1) & not emp s3 ) by A3;
then  ( pop s2 = G2 . (G1 . (pop s1)) & top s2 = F2 . (F1 . (top s1)) ) by A6, A7;
hence  ( pop s2 = (G2 * G1) . (pop s1) & top s2 = (F2 * F1) . (top s1) ) by A1, A2, FUNCT_1:13; ::_thesis: verum
end;
let e1 be Element of X1; ::_thesis: for e2 being Element of X3 st e2 = (F2 * F1) . e1 holds
push (e2,s2) = (G2 * G1) . (push (e1,s1))
let e2 be Element of X3; ::_thesis: ( e2 = (F2 * F1) . e1 implies push (e2,s2) = (G2 * G1) . (push (e1,s1)) )
reconsider e3 = F1 . e1 as Element of X2 by A1, FUNCT_1:def_3;
assume  e2 = (F2 * F1) . e1 ; ::_thesis: push (e2,s2) = (G2 * G1) . (push (e1,s1))
then A8: e2 = F2 . e3 by A1, FUNCT_1:13;
 push (e3,s3) = G1 . (push (e1,s1)) by A3;
then  push (e2,s2) = G2 . (G1 . (push (e1,s1))) by A7, A8, A6;
hence  push (e2,s2) = (G2 * G1) . (push (e1,s1)) by A2, FUNCT_1:13; ::_thesis: verum
end;

theorem Th45: :: STACKS_1:45
for X1, X2 being StackAlgebra
for F, G being Function st F,G form_isomorphism_between X1,X2 holds
for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
proof
let X1, X2 be StackAlgebra; ::_thesis: for F, G being Function st F,G form_isomorphism_between X1,X2 holds
for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
let F, G be Function; ::_thesis: ( F,G form_isomorphism_between X1,X2 implies for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.| )
assume that
A1: ( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one ) and
A2: ( dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one ) and
A3: for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = F . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ; :: according to STACKS_1:def_21 ::_thesis: for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
reconsider F1 = F as Function of the carrier of X1, the carrier of X2 by A1, FUNCT_2:2;
reconsider G1 = G as Function of the carrier' of X1, the carrier' of X2 by A2, FUNCT_2:2;
let s1 be stack of X1; ::_thesis: for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
defpred S1[ stack of X1] means  for s2 being stack of X2 st s2 = G . $1 holds
|.s2.| = F * |.$1.|;
A4: for s1 being stack of X1 st emp s1 holds
S1[s1]
proof
let s1 be stack of X1; ::_thesis: ( emp s1 implies S1[s1] )
assume A5: emp s1 ; ::_thesis: S1[s1]
let s2 be stack of X2; ::_thesis: ( s2 = G . s1 implies |.s2.| = F * |.s1.| )
assume  s2 = G . s1 ; ::_thesis: |.s2.| = F * |.s1.|
then  emp s2 by A3, A5;
then  ( |.s2.| = {} & |.s1.| = {} ) by A5, Th5;
hence  |.s2.| = F * |.s1.| ; ::_thesis: verum
end;
A6: for s1 being stack of X1
for e being Element of X1 st S1[s1] holds
S1[ push (e,s1)]
proof
let s1 be stack of X1; ::_thesis: for e being Element of X1 st S1[s1] holds
S1[ push (e,s1)]
let e be Element of X1; ::_thesis: ( S1[s1] implies S1[ push (e,s1)] )
assume A7: S1[s1] ; ::_thesis: S1[ push (e,s1)]
let s2 be stack of X2; ::_thesis: ( s2 = G . (push (e,s1)) implies |.s2.| = F * |.(push (e,s1)).| )
A8: |.(G1 . s1).| = F * |.s1.| by A7;
A9: <*(F1 . e)*> = F * <*e*> by A1, FINSEQ_2:34;
assume  s2 = G . (push (e,s1)) ; ::_thesis: |.s2.| = F * |.(push (e,s1)).|
then  s2 = push ((F1 . e),(G1 . s1)) by A3;
hence |.s2.| = <*(F1 . e)*> ^ |.(G1 . s1).| by Th8
.= F * (<*e*> ^ |.s1.|) by A8, A9, FINSEQOP:9
.= F * |.(push (e,s1)).| by Th8 ;
::_thesis: verum
end;
thus  S1[s1] from STACKS_1:sch_3(A4, A6); ::_thesis: verum
end;

definition
let X1, X2 be StackAlgebra;
predX1,X2 are_isomorphic  means :: STACKS_1:def 22
 ex F, G being Function st F,G form_isomorphism_between X1,X2;
reflexivity
 for X1 being StackAlgebra ex F, G being Function st F,G form_isomorphism_between X1,X1
proof
let X be StackAlgebra; ::_thesis: ex F, G being Function st F,G form_isomorphism_between X,X
take F = id the carrier of X; ::_thesis: ex G being Function st F,G form_isomorphism_between X,X
take G = id the carrier' of X; ::_thesis: F,G form_isomorphism_between X,X
thus  F,G form_isomorphism_between X,X by Th42; ::_thesis: verum
end;
symmetry
 for X1, X2 being StackAlgebra st ex F, G being Function st F,G form_isomorphism_between X1,X2 holds
ex F, G being Function st F,G form_isomorphism_between X2,X1
proof
let X1, X2 be StackAlgebra; ::_thesis: ( ex F, G being Function st F,G form_isomorphism_between X1,X2 implies ex F, G being Function st F,G form_isomorphism_between X2,X1 )
given F, G being Function such that A1: F,G form_isomorphism_between X1,X2 ; ::_thesis: ex F, G being Function st F,G form_isomorphism_between X2,X1
take  F " ; ::_thesis: ex G being Function st F " ,G form_isomorphism_between X2,X1
take  G " ; ::_thesis: F " ,G " form_isomorphism_between X2,X1
thus  F " ,G " form_isomorphism_between X2,X1 by A1, Th43; ::_thesis: verum
end;
end;

:: deftheorem  defines are_isomorphic STACKS_1:def_22_:_
 for X1, X2 being StackAlgebra holds
( X1,X2 are_isomorphic iff ex F, G being Function st F,G form_isomorphism_between X1,X2 );

theorem :: STACKS_1:46
for X1, X2, X3 being StackAlgebra st X1,X2 are_isomorphic & X2,X3 are_isomorphic holds
X1,X3 are_isomorphic
proof
let X1, X2, X3 be StackAlgebra; ::_thesis: ( X1,X2 are_isomorphic & X2,X3 are_isomorphic implies X1,X3 are_isomorphic )
given F1, G1 being Function such that A1: F1,G1 form_isomorphism_between X1,X2 ; :: according to STACKS_1:def_22 ::_thesis: ( not X2,X3 are_isomorphic or X1,X3 are_isomorphic )
given F2, G2 being Function such that A2: F2,G2 form_isomorphism_between X2,X3 ; :: according to STACKS_1:def_22 ::_thesis: X1,X3 are_isomorphic
take  F2 * F1 ; :: according to STACKS_1:def_22 ::_thesis: ex G being Function st F2 * F1,G form_isomorphism_between X1,X3
take  G2 * G1 ; ::_thesis: F2 * F1,G2 * G1 form_isomorphism_between X1,X3
thus  F2 * F1,G2 * G1 form_isomorphism_between X1,X3 by A1, A2, Th44; ::_thesis: verum
end;

theorem :: STACKS_1:47
for X1, X2 being StackAlgebra st X1,X2 are_isomorphic & X1 is proper-for-identity holds
X2 is proper-for-identity
proof
let X1, X2 be StackAlgebra; ::_thesis: ( X1,X2 are_isomorphic & X1 is proper-for-identity implies X2 is proper-for-identity )
given F, G being Function such that A1: F,G form_isomorphism_between X1,X2 ; :: according to STACKS_1:def_22 ::_thesis: ( not X1 is proper-for-identity or X2 is proper-for-identity )
assume A2: X1 is proper-for-identity ; ::_thesis: X2 is proper-for-identity
let s1, s2 be stack of X2; :: according to STACKS_1:def_15 ::_thesis: ( s1 == s2 implies s1 = s2 )
A3: ( dom G = the carrier' of X1 & rng G = the carrier' of X2 ) by A1, Def21;
then consider q1 being set  such that
A4: ( q1 in dom G & s1 = G . q1 ) by FUNCT_1:def_3;
consider q2 being set  such that
A5: ( q2 in dom G & s2 = G . q2 ) by A3, FUNCT_1:def_3;
reconsider q1 = q1, q2 = q2 as stack of X1 by A1, Def21, A4, A5;
A6: ( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one ) by A1, Def21;
A7: ( rng |.q1.| c= the carrier of X1 & rng |.q2.| c= the carrier of X1 ) ;
assume  |.s1.| = |.s2.| ; :: according to STACKS_1:def_14 ::_thesis: s1 = s2
then A8: F * |.q1.| = |.s2.| by A1, A4, Th45
.= F * |.q2.| by A1, A5, Th45 ;
 ( dom (F * |.q1.|) = dom |.q1.| & dom (F * |.q2.|) = dom |.q2.| ) by A6, A7, RELAT_1:27;
then  |.q1.| = |.q2.| by A6, A7, A8, FUNCT_1:27;
then  q1 == q2 by Def14;
hence  s1 = s2 by A2, A4, A5, Def15; ::_thesis: verum
end;

theorem Th48: :: STACKS_1:48
for X being proper-for-identity StackAlgebra ex G being Function st
( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
proof
let X be proper-for-identity StackAlgebra; ::_thesis: ex G being Function st
( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
deffunc H1( stack of X) ->  Element of the carrier of X * = |.$1.|;
consider G being Function of the carrier' of X,( the carrier of X *) such that
A1: for s being stack of X holds G . s = H1(s) from FUNCT_2:sch_4();
take  G ; ::_thesis: ( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
thus  for s being stack of X holds G . s = |.s.| by A1; ::_thesis: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
set F = id the carrier of X;
set X2 = StandardStackSystem the carrier of X;
set A = the carrier of X;
A2: ( the carrier of (StandardStackSystem the carrier of X) = the carrier of X & the carrier' of (StandardStackSystem the carrier of X) = the carrier of X * & ( for s being stack of (StandardStackSystem the carrier of X) 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 (StandardStackSystem the carrier of X) & pop s = {} ) ) & ( for e being Element of (StandardStackSystem the carrier of X) holds push (e,s) = <*e*> ^ g ) ) ) ) ) ) by Def7;
thus  ( dom (id the carrier of X) = the carrier of X & rng (id the carrier of X) = the carrier of (StandardStackSystem the carrier of X) & id the carrier of X is one-to-one ) by A2; :: according to STACKS_1:def_21 ::_thesis: ( dom G = the carrier' of X & rng G = the carrier' of (StandardStackSystem the carrier of X) & G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )
thus A3: dom G = the carrier' of X by FUNCT_2:def_1; ::_thesis: ( rng G = the carrier' of (StandardStackSystem the carrier of X) & G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )
thus  rng G = the carrier' of (StandardStackSystem the carrier of X) ::_thesis: ( G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )
proof
thus  rng G c= the carrier' of (StandardStackSystem the carrier of X) by A2; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of (StandardStackSystem the carrier of X) c= rng G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of (StandardStackSystem the carrier of X) or x in rng G )
assume  x in the carrier' of (StandardStackSystem the carrier of X) ; ::_thesis: x in rng G
then reconsider x = x as Element of the carrier of X * by Def7;
consider s being stack of X such that
A4: |.s.| = x by Th12;
 x = G . s by A1, A4;
hence  x in rng G by A3, FUNCT_1:def_3; ::_thesis: verum
end;
thus  G is one-to-one ::_thesis: for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom G or not b1 in dom G or not G . x = G . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom G or not y in dom G or not G . x = G . y or x = y )
assume  ( x in dom G & y in dom G ) ; ::_thesis: ( not G . x = G . y or x = y )
then reconsider s1 = x, s2 = y as stack of X ;
assume  G . x = G . y ; ::_thesis: x = y
then |.s1.| = G . y by A1
.= |.s2.| by A1 ;
then  s1 == s2 by Def14;
hence  x = y by Def15; ::_thesis: verum
end;
let s1 be stack of X; ::_thesis: for s2 being stack of (StandardStackSystem the carrier of X) st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
let s2 be stack of (StandardStackSystem the carrier of X); ::_thesis: ( s2 = G . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) )
assume  s2 = G . s1 ; ::_thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
then A5: s2 = |.s1.| by A1;
hereby  ::_thesis: ( ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
assume  emp s1 ; ::_thesis: emp s2
then  |.s1.| = {} by Th5;
hence  emp s2 by A5, Def7; ::_thesis: verum
end;
hereby  ::_thesis: ( not emp s1 iff ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) )
assume  emp s2 ; ::_thesis: emp s1
then  s2 = {} by Def7;
hence  emp s1 by A5, Th10; ::_thesis: verum
end;
hereby  ::_thesis: for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1))
assume A7: not emp s1 ; ::_thesis: ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) )
thus  pop s2 = Del (s2,1) by A7, A6, Def7
.= |.(pop s1).| by A5, A7, Th7
.= G . (pop s1) by A1 ; ::_thesis: top s2 = (id the carrier of X) . (top s1)
thus  top s2 = s2 . 1 by A7, A6, Def7
.= top s1 by A5, A7, Th9
.= (id the carrier of X) . (top s1) by FUNCT_1:18 ; ::_thesis: verum
end;
let e1 be Element of X; ::_thesis: for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1))
let e2 be Element of (StandardStackSystem the carrier of X); ::_thesis: ( e2 = (id the carrier of X) . e1 implies push (e2,s2) = G . (push (e1,s1)) )
assume  e2 = (id the carrier of X) . e1 ; ::_thesis: push (e2,s2) = G . (push (e1,s1))
hence  push (e2,s2) = <*((id the carrier of X) . e1)*> ^ s2 by Def7
.= <*e1*> ^ s2 by FUNCT_1:18
.= |.(push (e1,s1)).| by A5, Th8
.= G . (push (e1,s1)) by A1 ;
::_thesis: verum
end;

theorem :: STACKS_1:49
for X being proper-for-identity StackAlgebra holds X, StandardStackSystem the carrier of X are_isomorphic
proof
let X be proper-for-identity StackAlgebra; ::_thesis: X, StandardStackSystem the carrier of X are_isomorphic
consider G being Function such that
 for s being stack of X holds G . s = |.s.| and
A1: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X by Th48;
take  id the carrier of X ; :: according to STACKS_1:def_22 ::_thesis: ex G being Function st id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
take  G ; ::_thesis: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
thus  id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X by A1; ::_thesis: verum
end;