:: 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{ F₁() -> non empty set , P₁[ set ] } :

for p being FinSequence of F₁() holds P₁[p]

provided

A1: P₁[ <*> F₁()] and
A2: for p being FinSequence of F₁()
for x being Element of F₁() st P₁[p] holds
P₁[<*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 b₁ 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
[(b₁ . (x,y1)),(b₁ . (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 b₄ being Function of [:C,D:],D holds
( b₄ 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
[(b₄ . (x,y1)),(b₄ . (x,y2))] in R );

scheme :: STACKS_1:sch 2
LambdaD2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₃() } :

ex M being Function of [:F₁(),F₂():],F₃() st
for i being Element of F₁()
for j being Element of F₂() holds M . (i,j) = F₄(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 b₁ 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
b₁ . (x,y) = Class (R,(b . (x,y1)))

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (x,y) = Class (R,(b . (x,y1))) ) holds
b₁ = b₂

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 b₅ being Function of [:C,(Class R):],(Class R) holds
( b₅ = b /\/ R iff for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b₅ . (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 c₁ is strict ;
struct StackSystem -> 2-sorted ;
aggr StackSystem(# carrier, carrier', s_empty, s_push, s_pop, s_top #) -> StackSystem ;
sel s_empty c₁ -> Subset of the carrier' of c₁;
sel s_push c₁ -> Function of [: the carrier of c₁, the carrier' of c₁:], the carrier' of c₁;
sel s_pop c₁ -> Function of the carrier' of c₁, the carrier' of c₁;
sel s_top c₁ -> Function of the carrier' of c₁, the carrier of c₁;

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 b₁ being StackSystem st
( not b₁ is empty & not b₁ is void & b₁ 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 b₁ being non empty non void strict StackSystem st
( the carrier of b₁ = A & the carrier' of b₁ = A * & ( for s being stack of b₁ 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 b₁ & pop s = {} ) ) & ( for e being Element of b₁ holds push (e,s) = <*e*> ^ g ) ) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty non void strict StackSystem st the carrier of b₁ = A & the carrier' of b₁ = A * & ( for s being stack of b₁ 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 b₁ & pop s = {} ) ) & ( for e being Element of b₁ holds push (e,s) = <*e*> ^ g ) ) ) ) ) & the carrier of b₂ = A & the carrier' of b₂ = A * & ( for s being stack of b₂ 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 b₂ & pop s = {} ) ) & ( for e being Element of b₂ holds push (e,s) = <*e*> ^ g ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem EXAM defines StandardStackSystem STACKS_1:def 7 :
for A being non empty set
for b₂ being non empty non void strict StackSystem holds
( b₂ = StandardStackSystem A iff ( the carrier of b₂ = A & the carrier' of b₂ = A * & ( for s being stack of b₂ 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 b₂ & pop s = {} ) ) & ( for e being Element of b₂ 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 b₁ being stack of (StandardStackSystem A) holds
( b₁ is Relation-like & b₁ 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 b₁ being stack of (StandardStackSystem A) holds b₁ 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 b₁ being non empty non void StackSystem st
( b₁ is pop-finite & b₁ is push-pop & b₁ is top-push & b₁ is pop-push & b₁ is push-non-empty & b₁ 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{ F₁() -> StackAlgebra, F₂() -> stack of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

P1: for s being stack of F₁() st emp s holds
P₁[s] and
P2: for s being stack of F₁()
for e being Element of F₁() st P₁[s] holds
P₁[ push (e,s)]

proof end;

scheme :: STACKS_1:sch 4
EXsch{ F₁() -> StackAlgebra, F₂() -> stack of F₁(), F₃() -> non empty set , F₄() -> Element of F₃(), F₅( set , set ) -> Element of F₃() } :

ex a being Element of F₃() ex F being Function of the carrier' of F₁(),F₃() st
( a = F . F₂() & ( for s1 being stack of F₁() st emp s1 holds
F . s1 = F₄() ) & ( for s1 being stack of F₁()
for e being Element of F₁() holds F . (push (e,s1)) = F₅(e,(F . s1)) ) )

proof end;

scheme :: STACKS_1:sch 5
UNIQsch{ F₁() -> StackAlgebra, F₂() -> stack of F₁(), F₃() -> non empty set , F₄() -> Element of F₃(), F₅( set , set ) -> Element of F₃() } :

for a1, a2 being Element of F₃() st ex F being Function of the carrier' of F₁(),F₃() st
( a1 = F . F₂() & ( for s1 being stack of F₁() st emp s1 holds
F . s1 = F₄() ) & ( for s1 being stack of F₁()
for e being Element of F₁() holds F . (push (e,s1)) = F₅(e,(F . s1)) ) ) & ex F being Function of the carrier' of F₁(),F₃() st
( a2 = F . F₂() & ( for s1 being stack of F₁() st emp s1 holds
F . s1 = F₄() ) & ( for s1 being stack of F₁()
for e being Element of F₁() holds F . (push (e,s1)) = F₅(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 b₁ being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( b₁ = 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 b₁, b₂ being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st
( b₁ = 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
( b₂ = 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
b₁ = b₂

proof end;

end;

:: deftheorem MOD defines |. STACKS_1:def 13 :
for X being StackAlgebra
for s being stack of X
for b₃ being Element of the carrier of X * holds
( b₃ = |.s.| iff ex F being Function of the carrier' of X,( the carrier of X *) st
( b₃ = 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 b₁ being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in b₁ iff s1 == s2 )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier' of X st ( for s1, s2 being stack of X holds
( [s1,s2] in b₁ iff s1 == s2 ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in b₂ iff s1 == s2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem REL defines ==_ STACKS_1:def 16 :
for X being StackAlgebra
for b₂ being Relation of the carrier' of X holds
( b₂ = ==_ X iff for s1, s2 being stack of X holds
( [s1,s2] in b₂ 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 b₁ being Subset of the carrier' of X st
( s in b₁ & ( for e being Element of X
for s1 being stack of X st s1 in b₁ holds
( push (e,s1) in b₁ & ( not emp s1 implies pop s1 in b₁ ) ) ) & ( 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
b₁ c= A ) )

proof end;

uniqueness
for b₁, b₂ being Subset of the carrier' of X st s in b₁ & ( for e being Element of X
for s1 being stack of X st s1 in b₁ holds
( push (e,s1) in b₁ & ( not emp s1 implies pop s1 in b₁ ) ) ) & ( 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
b₁ c= A ) & s in b₂ & ( for e being Element of X
for s1 being stack of X st s1 in b₂ holds
( push (e,s1) in b₂ & ( not emp s1 implies pop s1 in b₂ ) ) ) & ( 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
b₂ c= A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem COSET defines coset STACKS_1:def 17 :
for X being StackAlgebra
for s being stack of X
for b₃ being Subset of the carrier' of X holds
( b₃ = coset s iff ( s in b₃ & ( for e being Element of X
for s1 being stack of X st s1 in b₃ holds
( push (e,s1) in b₃ & ( not emp s1 implies pop s1 in b₃ ) ) ) & ( 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
b₃ 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 b₁ being RedSequence of R st b₁ 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 b₁ being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in b₁ iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier' of X st ( for s1, s2 being stack of X holds
( [s1,s2] in b₁ 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 b₂ iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem CRED defines ConstructionRed STACKS_1:def 18 :
for X being StackAlgebra
for b₂ being Relation of the carrier' of X holds
( b₂ = ConstructionRed X iff for s1, s2 being stack of X holds
( [s1,s2] in b₂ 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{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Relation of F₁(), P₁[ set ] } :

P₁[F₃()]

provided

W1: P₁[F₂()] and
W2: F₄() reduces F₂(),F₃() and
W3: for x, y being Element of F₁() st F₄() reduces F₂(),x & [x,y] in F₄() & P₁[x] holds
P₁[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 b₁ being stack of X st
( emp b₁ & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b₁ & ( 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 b₁, b₂ being stack of X st emp b₁ & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b₁ & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp b₂ & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b₂ & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem CORE defines core STACKS_1:def 19 :
for X being StackAlgebra
for s, b₃ being stack of X holds
( b₃ = core s iff ( emp b₃ & ex t being the carrier' of b₁ -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = b₃ & ( 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 b₁, b₂ being strict StackSystem st the carrier of b₁ = the carrier of X & the carrier' of b₁ = Class (==_ X) & the s_empty of b₁ = { the s_empty of X} & the s_push of b₁ = the s_push of X /\/ (==_ X) & the s_pop of b₁ = ( 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 b₁ = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) & the carrier of b₂ = the carrier of X & the carrier' of b₂ = Class (==_ X) & the s_empty of b₂ = { the s_empty of X} & the s_push of b₂ = the s_push of X /\/ (==_ X) & the s_pop of b₂ = ( 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 b₂ = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being strict StackSystem st
( the carrier of b₁ = the carrier of X & the carrier' of b₁ = Class (==_ X) & the s_empty of b₁ = { the s_empty of X} & the s_push of b₁ = the s_push of X /\/ (==_ X) & the s_pop of b₁ = ( 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 b₁ = ( 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 b₂ being strict StackSystem holds
( b₂ = X /== iff ( the carrier of b₂ = the carrier of X & the carrier' of b₂ = Class (==_ X) & the s_empty of b₂ = { the s_empty of X} & the s_push of b₂ = the s_push of X /\/ (==_ X) & the s_pop of b₂ = ( 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 b₂ = ( 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 b₁ being StackAlgebra st b₁ 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;