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


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 *
proofend;
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 *
proofend;
end;

theorem Th1: :: STACKS_1:1
for i being Nat holds Del ({},i) = {}
proofend;

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]
proofend;

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
proofend;
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)
proofend;

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 &amp; y in Class R &amp; 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 &amp; y in Class R &amp; y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1)))
proofend;
uniqueness
 for b1, b2 being Function of [:C,(Class R):],(Class R) st ( for x, y, y1 being set st x in C &amp; y in Class R &amp; y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) ) &amp; ( for x, y, y1 being set st x in C &amp; y in Class R &amp; y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ) holds
b1 = b2
proofend;
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 &amp; y in Class R &amp; 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
proofend;
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 &amp; not b1 is void &amp; b1 is strict )
proofend;
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 &amp; the carrier' of it = A * &amp; ( for s being stack of it holds
( ( emp s implies s is empty ) &amp; ( s is empty implies emp s ) &amp; ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 &amp; pop s = Del (g,1) ) ) &amp; ( emp s implies ( top s = the Element of it &amp; pop s = {} ) ) &amp; ( 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 &amp; the carrier' of b1 = A * &amp; ( for s being stack of b1 holds
( ( emp s implies s is empty ) &amp; ( s is empty implies emp s ) &amp; ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 &amp; pop s = Del (g,1) ) ) &amp; ( emp s implies ( top s = the Element of b1 &amp; pop s = {} ) ) &amp; ( for e being Element of b1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty non void strict StackSystem st the carrier of b1 = A &amp; the carrier' of b1 = A * &amp; ( for s being stack of b1 holds
( ( emp s implies s is empty ) &amp; ( s is empty implies emp s ) &amp; ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 &amp; pop s = Del (g,1) ) ) &amp; ( emp s implies ( top s = the Element of b1 &amp; pop s = {} ) ) &amp; ( for e being Element of b1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) &amp; the carrier of b2 = A &amp; the carrier' of b2 = A * &amp; ( for s being stack of b2 holds
( ( emp s implies s is empty ) &amp; ( s is empty implies emp s ) &amp; ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 &amp; pop s = Del (g,1) ) ) &amp; ( emp s implies ( top s = the Element of b2 &amp; pop s = {} ) ) &amp; ( for e being Element of b2 holds push (e,s) = <*e*> ^ g ) ) ) ) ) holds
b1 = b2
proofend;
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 &amp; the carrier' of b2 = A * &amp; ( for s being stack of b2 holds
( ( emp s implies s is empty ) &amp; ( s is empty implies emp s ) &amp; ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 &amp; pop s = Del (g,1) ) ) &amp; ( emp s implies ( top s = the Element of b2 &amp; pop s = {} ) ) &amp; ( 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
proofend;
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
proofend;
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 &amp; ( 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 &amp; ( 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
proofend;
cluster StandardStackSystem A ->  non empty non void strict push-pop ;
coherence
 StandardStackSystem A is push-pop
proofend;
cluster StandardStackSystem A ->  non empty non void strict top-push ;
coherence
 StandardStackSystem A is top-push
proofend;
cluster StandardStackSystem A ->  non empty non void strict pop-push ;
coherence
 StandardStackSystem A is pop-push
proofend;
cluster StandardStackSystem A ->  non empty non void strict push-non-empty ;
coherence
 StandardStackSystem A is push-non-empty
proofend;
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 &amp; b1 is push-pop &amp; b1 is top-push &amp; b1 is pop-push &amp; b1 is push-non-empty &amp; b1 is strict )
proofend;
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
proofend;

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
proofend;
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 &amp; X is pop-push &amp; push (e1,s1) = push (e2,s2) holds
( e1 = e2 &amp; s1 = s2 )
proofend;

theorem :: STACKS_1:4
for X being non empty non void StackSystem
for s1, s2 being stack of X st X is push-pop &amp; not emp s1 &amp; not emp s2 &amp; pop s1 = pop s2 &amp; top s1 = top s2 holds
s1 = s2
proofend;

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)]
proofend;

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() &amp; ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) &amp; ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) )
proofend;

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() &amp; ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) &amp; ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) &amp; ex F being Function of the carrier' of F1(),F3() st
( a2 = F . F2() &amp; ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) &amp; ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) holds
a1 = a2
proofend;

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 &amp; ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) &amp; ( 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 &amp; ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) &amp; ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) )
proofend;
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 &amp; ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) &amp; ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) &amp; ex F being Function of the carrier' of X,( the carrier of X *) st
( b2 = F . s &amp; ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) &amp; ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) holds
b1 = b2
proofend;
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 &amp; ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) &amp; ( 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.| = {}
proofend;

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).|
proofend;

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)
proofend;

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.|
proofend;

theorem Th9: :: STACKS_1:9
for X being StackAlgebra
for s being stack of X st not emp s holds
top s = |.s.| . 1
proofend;

theorem Th10: :: STACKS_1:10
for X being StackAlgebra
for s being stack of X st |.s.| = {} holds
emp s
proofend;

theorem Th11: :: STACKS_1:11
for A being non empty set
for s being stack of (StandardStackSystem A) holds |.s.| = s
proofend;

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

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 &amp; s2 == s3 holds
s1 == s3
proofend;

theorem Th14: :: STACKS_1:14
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 &amp; emp s1 holds
emp s2
proofend;

theorem Th15: :: STACKS_1:15
for X being StackAlgebra
for s1, s2 being stack of X st emp s1 &amp; emp s2 holds
s1 == s2
proofend;

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)
proofend;

theorem Th17: :: STACKS_1:17
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 &amp; not emp s1 holds
pop s1 == pop s2
proofend;

theorem Th18: :: STACKS_1:18
for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 &amp; not emp s1 holds
top s1 = top s2
proofend;

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
proofend;
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 )
proofend;
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 ) ) &amp; ( for s1, s2 being stack of X holds
( [s1,s2] in b2 iff s1 == s2 ) ) holds
b1 = b2
proofend;
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 &amp; ==_ X is symmetric &amp; ==_ X is transitive )
proofend;
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
proofend;

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 &amp; ( for e being Element of X
for s1 being stack of X st s1 in it holds
( push (e,s1) in it &amp; ( not emp s1 implies pop s1 in it ) ) ) &amp; ( for A being Subset of the carrier' of X st s in A &amp; ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A &amp; ( 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 &amp; ( for e being Element of X
for s1 being stack of X st s1 in b1 holds
( push (e,s1) in b1 &amp; ( not emp s1 implies pop s1 in b1 ) ) ) &amp; ( for A being Subset of the carrier' of X st s in A &amp; ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A &amp; ( not emp s1 implies pop s1 in A ) ) ) holds
b1 c= A ) )
proofend;
uniqueness
 for b1, b2 being Subset of the carrier' of X st s in b1 &amp; ( for e being Element of X
for s1 being stack of X st s1 in b1 holds
( push (e,s1) in b1 &amp; ( not emp s1 implies pop s1 in b1 ) ) ) &amp; ( for A being Subset of the carrier' of X st s in A &amp; ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A &amp; ( not emp s1 implies pop s1 in A ) ) ) holds
b1 c= A ) &amp; s in b2 &amp; ( for e being Element of X
for s1 being stack of X st s1 in b2 holds
( push (e,s1) in b2 &amp; ( not emp s1 implies pop s1 in b2 ) ) ) &amp; ( for A being Subset of the carrier' of X st s in A &amp; ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A &amp; ( not emp s1 implies pop s1 in A ) ) ) holds
b2 c= A ) holds
b1 = b2
proofend;
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 &amp; ( for e being Element of X
for s1 being stack of X st s1 in b3 holds
( push (e,s1) in b3 &amp; ( not emp s1 implies pop s1 in b3 ) ) ) &amp; ( for A being Subset of the carrier' of X st s in A &amp; ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A &amp; ( 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 ) &amp; ( not emp s &amp; pop s in coset s1 implies s in coset s1 ) )
proofend;

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)) &amp; ( not emp s implies s in coset (pop s) ) )
proofend;

theorem :: STACKS_1:22
for X being StackAlgebra
for s being stack of X ex s1 being stack of X st
( emp s1 &amp; s1 in coset s )
proofend;

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
proofend;
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 &amp; 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 &amp; s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) )
proofend;
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 &amp; s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) &amp; ( for s1, s2 being stack of X holds
( [s1,s2] in b2 iff ( ( not emp s1 &amp; s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) holds
b1 = b2
proofend;
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 &amp; 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 )
proofend;

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 &amp; [x,y] in F4() &amp; P1[x] holds
P1[y]
proofend;

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

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  }
proofend;

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 &amp; ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s &amp; t . (len t) = it &amp; ( for i being Nat st 1 <= i &amp; i < len t holds
( not emp t /. i &amp; t /. (i + 1) = pop (t /. i) ) ) ) );
existence
 ex b1 being stack of X st
( emp b1 &amp; ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s &amp; t . (len t) = b1 &amp; ( for i being Nat st 1 <= i &amp; i < len t holds
( not emp t /. i &amp; t /. (i + 1) = pop (t /. i) ) ) ) )
proofend;
uniqueness
 for b1, b2 being stack of X st emp b1 &amp; ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s &amp; t . (len t) = b1 &amp; ( for i being Nat st 1 <= i &amp; i < len t holds
( not emp t /. i &amp; t /. (i + 1) = pop (t /. i) ) ) ) &amp; emp b2 &amp; ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s &amp; t . (len t) = b2 &amp; ( for i being Nat st 1 <= i &amp; i < len t holds
( not emp t /. i &amp; t /. (i + 1) = pop (t /. i) ) ) ) holds
b1 = b2
proofend;
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 &amp; ex t being the carrier' of b1 -valued RedSequence of ConstructionRed X st
( t . 1 = s &amp; t . (len t) = b3 &amp; ( for i being Nat st 1 <= i &amp; i < len t holds
( not emp t /. i &amp; 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
proofend;

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

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

theorem Th29: :: STACKS_1:29
for X being StackAlgebra
for s being stack of X holds core s in coset s
proofend;

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 &amp; s1 in coset s )
proofend;

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

theorem Th32: :: STACKS_1:32
for X being StackAlgebra
for s1, s, s2 being stack of X st s1 in coset s &amp; s2 in coset s &amp; |.s1.| = |.s2.| holds
s1 = s2
proofend;

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}
proofend;

begin

definition
let X be StackAlgebra;
funcX /==  ->  strict StackSystem  means :Def20: :: STACKS_1:def 20
( the carrier of it = the carrier of X &amp; the carrier' of it = Class (==_ X) &amp; the s_empty of it = { the s_empty of X} &amp; the s_push of it = the s_push of X /\/ (==_ X) &amp; the s_pop of it = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) &amp; ( 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 &amp; the carrier' of b1 = Class (==_ X) &amp; the s_empty of b1 = { the s_empty of X} &amp; the s_push of b1 = the s_push of X /\/ (==_ X) &amp; the s_pop of b1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) &amp; ( 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) ) &amp; the carrier of b2 = the carrier of X &amp; the carrier' of b2 = Class (==_ X) &amp; the s_empty of b2 = { the s_empty of X} &amp; the s_push of b2 = the s_push of X /\/ (==_ X) &amp; the s_pop of b2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) &amp; ( 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
proofend;
existence
 ex b1 being strict StackSystem st
( the carrier of b1 = the carrier of X &amp; the carrier' of b1 = Class (==_ X) &amp; the s_empty of b1 = { the s_empty of X} &amp; the s_push of b1 = the s_push of X /\/ (==_ X) &amp; the s_pop of b1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) &amp; ( 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) ) )
proofend;
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 &amp; the carrier' of b2 = Class (==_ X) &amp; the s_empty of b2 = { the s_empty of X} &amp; the s_push of b2 = the s_push of X /\/ (==_ X) &amp; the s_pop of b2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) &amp; ( 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 &amp; not X /== is void )
proofend;
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)
proofend;

theorem Th35: :: STACKS_1:35
for X being StackAlgebra
for s being stack of X holds Class ((==_ X),s) is stack of (X /==)
proofend;

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 )
proofend;

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 )
proofend;

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) &amp; E = e holds
( push (e,s) in push (E,S) &amp; Class ((==_ X),(push (e,s))) = push (E,S) )
proofend;

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) &amp; not emp s holds
( pop s in pop S &amp; Class ((==_ X),(pop s)) = pop S )
proofend;

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) &amp; not emp s holds
top S = top s
proofend;

registration
let X be StackAlgebra;
clusterX /==  ->  strict pop-finite ;
coherence
 X /== is pop-finite
proofend;
clusterX /==  ->  strict push-pop ;
coherence
 X /== is push-pop
proofend;
clusterX /==  ->  strict top-push ;
coherence
 X /== is top-push
proofend;
clusterX /==  ->  strict pop-push ;
coherence
 X /== is pop-push
proofend;
clusterX /==  ->  strict push-non-empty ;
coherence
 X /== is push-non-empty
proofend;
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.|
proofend;

registration
let X be StackAlgebra;
clusterX /==  ->  strict proper-for-identity ;
coherence
 X /== is proper-for-identity
proofend;
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
proofend;
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 &amp; rng F = the carrier of X2 &amp; F is one-to-one &amp; dom G = the carrier' of X1 &amp; rng G = the carrier' of X2 &amp; G is one-to-one &amp; ( for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) &amp; ( emp s2 implies emp s1 ) &amp; ( not emp s1 implies ( pop s2 = G . (pop s1) &amp; top s2 = F . (top s1) ) ) &amp; ( 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 &amp; rng F = the carrier of X2 &amp; F is one-to-one &amp; dom G = the carrier' of X1 &amp; rng G = the carrier' of X2 &amp; G is one-to-one &amp; ( for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) &amp; ( emp s2 implies emp s1 ) &amp; ( not emp s1 implies ( pop s2 = G . (pop s1) &amp; top s2 = F . (top s1) ) ) &amp; ( 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
proofend;

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

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 &amp; F2,G2 form_isomorphism_between X2,X3 holds
F2 * F1,G2 * G1 form_isomorphism_between X1,X3
proofend;

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.|
proofend;

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
proofend;
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
proofend;
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 &amp; X2,X3 are_isomorphic holds
X1,X3 are_isomorphic
proofend;

theorem :: STACKS_1:47
for X1, X2 being StackAlgebra st X1,X2 are_isomorphic &amp; X1 is proper-for-identity holds
X2 is proper-for-identity
proofend;

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.| ) &amp; id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
proofend;

theorem :: STACKS_1:49
for X being proper-for-identity StackAlgebra holds X, StandardStackSystem the carrier of X are_isomorphic
proofend;