:: Representation Theorem for Stacks
:: by Grzegorz Bancerek
::
:: Received February 22, 2011
:: Copyright (c) 2011 Association of Mizar Users


begin

definition
let A be set ;
let s1, s2 be FinSequence of A;
:: original: ^
redefine func s1 ^ s2 -> Element of A * ;
coherence
s1 ^ s2 is Element of A *
proof 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 end;
end;

theorem Lem1: :: STACKS_1:1
for i being Nat holds Del ({},i) = {}
proof end;

theorem FINSEQp2150: :: STACKS_1:2
for D being non empty set
for s being FinSequence of D st s <> {} holds
ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w
proof 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 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 :Def2: :: 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 end;
end;

:: deftheorem Def2 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 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 ;
func b /\/ R -> Function of [:C,(Class R):],(Class R) means :Def4: :: 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 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 end;
end;

:: deftheorem Def4 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 func f +* g -> Function of A,B;
coherence
f +* g is Function of A,B
proof end;
end;

begin

definition
attr c1 is strict ;
struct StackSystem -> 2-sorted ;
aggr StackSystem(# 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 StackSystem ;
existence
ex b1 being StackSystem st
( not b1 is empty & not b1 is void & b1 is strict )
proof end;
end;

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

definition
let X be non empty non void StackSystem ;
let s be stack of X;
pred emp s means :EMP: :: STACKS_1:def 3
s in the s_empty 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
;
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 EMP defines emp STACKS_1:def 3 :
for X being non empty non void StackSystem
for s being stack of X holds
( emp s iff s in the s_empty of X );

:: deftheorem defines pop STACKS_1:def 4 :
for X being non empty 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 empty non void StackSystem
for s being stack of X holds top s = the s_top of X . s;

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

:: deftheorem EXAM 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 -> Relation-like Function-like Element of the carrier' of (StandardStackSystem A);
coherence
for b1 being stack of (StandardStackSystem A) holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

registration
let A be non empty set ;
cluster -> FinSequence-like Element of the carrier' of (StandardStackSystem A);
coherence
for b1 being stack of (StandardStackSystem A) holds b1 is FinSequence-like
proof end;
end;

for A being non empty set
for m being stack of (StandardStackSystem A) holds
( emp m iff m = {} )
by EXAM;

for A being non empty set
for c being Element of (StandardStackSystem A)
for m being stack of (StandardStackSystem A) holds push (c,m) = <*c*> ^ m
by EXAM;

for A being non empty set
for m being stack of (StandardStackSystem A) st not emp m holds
pop m = Del (m,1)
by EXAM;

definition
let X be non empty non void StackSystem ;
attr X is pop-finite means :POPFIN: :: 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 ) );
attr X is push-pop means :PUSHPOP: :: STACKS_1:def 9
for s being stack of X st not emp s holds
s = push ((top s),(pop s));
attr X is top-push means :TOPPUSH: :: STACKS_1:def 10
for s being stack of X
for e being Element of X holds e = top (push (e,s));
attr X is pop-push means :POPPUSH: :: STACKS_1:def 11
for s being stack of X
for e being Element of X holds s = pop (push (e,s));
attr X is push-non-empty means :PUSHNE: :: STACKS_1:def 12
for s being stack of X
for e being Element of X holds not emp push (e,s);
end;

:: deftheorem POPFIN 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 PUSHPOP 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 TOPPUSH 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 POPPUSH 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 PUSHNE 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 end;
cluster StandardStackSystem A -> non empty non void strict push-pop ;
coherence
StandardStackSystem A is push-pop
proof end;
cluster StandardStackSystem A -> non empty non void strict top-push ;
coherence
StandardStackSystem A is top-push
proof end;
cluster StandardStackSystem A -> non empty non void strict pop-push ;
coherence
StandardStackSystem A is pop-push
proof end;
cluster StandardStackSystem A -> non empty non void strict push-non-empty ;
coherence
StandardStackSystem A is push-non-empty
proof end;
end;

registration
cluster non empty non void strict pop-finite push-pop top-push pop-push push-non-empty 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 end;
end;

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

theorem Th1: :: STACKS_1:3
for X being non empty non void StackSystem st X is pop-finite holds
ex s being stack of X st emp s
proof 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 end;
end;

theorem Th2: :: STACKS_1:4
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 end;

theorem :: STACKS_1:5
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 end;

begin

scheme :: STACKS_1:sch 3
INDsch{ F1() -> StackAlgebra, F2() -> stack of F1(), P1[ set ] } :
P1[F2()]
provided
P1: for s being stack of F1() st emp s holds
P1[s] and
P2: for s being stack of F1()
for e being Element of F1() st P1[s] holds
P1[ push (e,s)]
proof 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 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 end;

begin

definition
let X be StackAlgebra;
let s be stack of X;
func |.s.| -> Element of the carrier of X * means :MOD: :: 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 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 end;
end;

:: deftheorem MOD 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 Th31: :: STACKS_1:6
for X being StackAlgebra
for s being stack of X st emp s holds
|.s.| = {}
proof end;

theorem Th32: :: STACKS_1:7
for X being StackAlgebra
for s being stack of X st not emp s holds
|.s.| = <*(top s)*> ^ |.(pop s).|
proof end;

theorem Th33: :: STACKS_1:8
for X being StackAlgebra
for s being stack of X st not emp s holds
|.(pop s).| = Del (|.s.|,1)
proof end;

theorem Th34: :: STACKS_1:9
for X being StackAlgebra
for s being stack of X
for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
proof end;

theorem Th35: :: STACKS_1:10
for X being StackAlgebra
for s being stack of X st not emp s holds
top s = |.s.| . 1
proof end;

theorem Th351: :: STACKS_1:11
for X being StackAlgebra
for s being stack of X st |.s.| = {} holds
emp s
proof end;

theorem ThZ: :: STACKS_1:12
for A being non empty set
for s being stack of (StandardStackSystem A) holds |.s.| = s
proof end;

theorem Th36: :: STACKS_1:13
for X being StackAlgebra
for x being Element of the carrier of X * ex s being stack of X st |.s.| = x
proof end;

definition
let X be StackAlgebra;
let s1, s2 be stack of X;
pred s1 == s2 means :CONG: :: 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 CONG defines == STACKS_1:def 14 :
for X being StackAlgebra
for s1, s2 being stack of X holds
( s1 == s2 iff |.s1.| = |.s2.| );

theorem Th41: :: STACKS_1:14
for X being StackAlgebra
for s1, s2, s3 being stack of X st s1 == s2 & s2 == s3 holds
s1 == s3
proof end;

theorem Th42: :: STACKS_1:15
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & emp s1 holds
emp s2
proof end;

theorem Th43: :: STACKS_1:16
for X being StackAlgebra
for s1, s2 being stack of X st emp s1 & emp s2 holds
s1 == s2
proof end;

theorem Th44: :: STACKS_1:17
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 end;

theorem Th45: :: STACKS_1:18
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
pop s1 == pop s2
proof end;

theorem Th46: :: STACKS_1:19
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
top s1 = top s2
proof end;

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

:: deftheorem PROP 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 end;
end;

definition
let X be StackAlgebra;
func ==_ X -> Relation of the carrier' of X means :REL: :: 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 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 end;
end;

:: deftheorem REL 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 end;
end;

theorem Th50: :: STACKS_1:20
for X being StackAlgebra
for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
proof end;

definition
let X be StackAlgebra;
let s be stack of X;
func coset s -> Subset of the carrier' of X means :COSET: :: 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 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 end;
end;

:: deftheorem COSET 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 Th53: :: STACKS_1:21
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 end;

theorem :: STACKS_1:22
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 end;

theorem :: STACKS_1:23
for X being StackAlgebra
for s being stack of X ex s1 being stack of X st
( emp s1 & s1 in coset s )
proof end;

registration
let A be non empty set ;
let R be Relation of A;
cluster Relation-like A -valued Function-like non empty V43() FinSequence-like FinSubsequence-like RedSequence of R;
existence
ex b1 being RedSequence of R st b1 is A -valued
proof end;
end;

definition
let X be StackAlgebra;
func ConstructionRed X -> Relation of the carrier' of X means :CRED: :: 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 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 end;
end;

:: deftheorem CRED 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 Lem2: :: STACKS_1:24
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 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
W1: P1[F2()] and
W2: F4() reduces F2(),F3() and
W3: for x, y being Element of F1() st F4() reduces F2(),x & [x,y] in F4() & P1[x] holds
P1[y]
proof end;

theorem Th57: :: STACKS_1:25
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 end;

theorem Th58: :: STACKS_1:26
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 end;

definition
let X be StackAlgebra;
let s be stack of X;
func core s -> stack of X means :CORE: :: 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 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 end;
end;

:: deftheorem CORE 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 Th11: :: STACKS_1:27
for X being StackAlgebra
for s being stack of X st emp s holds
core s = s
proof end;

theorem Th12: :: STACKS_1:28
for X being StackAlgebra
for s being stack of X
for e being Element of X holds core (push (e,s)) = core s
proof end;

theorem Th13: :: STACKS_1:29
for X being StackAlgebra
for s being stack of X st not emp s holds
core (pop s) = core s
proof end;

theorem Th59a: :: STACKS_1:30
for X being StackAlgebra
for s being stack of X holds core s in coset s
proof end;

theorem Th17: :: STACKS_1:31
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 end;

theorem Th14: :: STACKS_1:32
for X being StackAlgebra
for s1, s being stack of X st s1 in coset s holds
core s1 = core s
proof end;

theorem Th15: :: STACKS_1:33
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 end;

theorem Th60: :: STACKS_1:34
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 end;

begin

definition
let X be StackAlgebra;
func X /== -> strict StackSystem means :QUOT: :: 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 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 end;
end;

:: deftheorem QUOT 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;
cluster X /== -> non empty non void strict ;
coherence
( not X /== is empty & not X /== is void )
proof end;
end;

theorem Th70: :: STACKS_1:35
for X being StackAlgebra
for S being stack of (X /==) ex s being stack of X st S = Class ((==_ X),s)
proof end;

theorem Th70a: :: STACKS_1:36
for X being StackAlgebra
for s being stack of X holds Class ((==_ X),s) is stack of (X /==)
proof end;

theorem Th71: :: STACKS_1:37
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 end;

theorem Th71a: :: STACKS_1:38
for X being StackAlgebra
for S being stack of (X /==) holds
( emp S iff S = the s_empty of X )
proof end;

theorem Th72: :: STACKS_1:39
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 end;

theorem Th73: :: 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
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
proof end;

theorem Th74: :: STACKS_1:41
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 end;

registration
let X be StackAlgebra;
cluster X /== -> strict pop-finite ;
coherence
X /== is pop-finite
proof end;
cluster X /== -> strict push-pop ;
coherence
X /== is push-pop
proof end;
cluster X /== -> strict top-push ;
coherence
X /== is top-push
proof end;
cluster X /== -> strict pop-push ;
coherence
X /== is pop-push
proof end;
cluster X /== -> strict push-non-empty ;
coherence
X /== is push-non-empty
proof end;
end;

theorem Th80: :: STACKS_1:42
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 end;

registration
let X be StackAlgebra;
cluster X /== -> strict proper-for-identity ;
coherence
X /== is proper-for-identity
proof end;
end;

registration
cluster non empty non void pop-finite push-pop top-push pop-push push-non-empty proper-for-identity StackSystem ;
existence
ex b1 being StackAlgebra st b1 is proper-for-identity
proof end;
end;

begin

definition
let X1, X2 be StackAlgebra;
let F, G be Function;
pred F,G form_isomorphism_between X1,X2 means :ISO: :: 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 ISO 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 ThI1: :: STACKS_1:43
for X being StackAlgebra holds id the carrier of X, id the carrier' of X form_isomorphism_between X,X
proof end;

theorem ThI2: :: STACKS_1:44
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 end;

theorem Th90: :: STACKS_1:45
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 end;

theorem Th97: :: STACKS_1:46
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 end;

definition
let X1, X2 be StackAlgebra;
pred X1,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 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 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:47
for X1, X2, X3 being StackAlgebra st X1,X2 are_isomorphic & X2,X3 are_isomorphic holds
X1,X3 are_isomorphic
proof end;

theorem :: STACKS_1:48
for X1, X2 being StackAlgebra st X1,X2 are_isomorphic & X1 is proper-for-identity holds
X2 is proper-for-identity
proof end;

theorem Th100: :: STACKS_1:49
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 end;

theorem :: STACKS_1:50
for X being proper-for-identity StackAlgebra holds X, StandardStackSystem the carrier of X are_isomorphic
proof end;