:: 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;