:: by Grzegorz Bancerek

::

:: Received February 22, 2011

:: Copyright (c) 2011-2018 Association of Mizar Users

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 *

end;
let s1, s2 be FinSequence of A;

:: original: ^

redefine func s1 ^ s2 -> Element of A * ;

coherence

s1 ^ s2 is Element of A *

proof 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 *

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

definition

let C, D be non empty set ;

let R be Relation;

ex b_{1} 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_{1} . (x,y1)),(b_{1} . (x,y2))] in R

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

ex b

for x being Element of C

for y1, y2 being Element of D st [y1,y2] in R holds

[(b

proof end;

:: deftheorem Def1 defines BinOp STACKS_1:def 1 :

for C, D being non empty set

for R being Relation

for b_{4} being Function of [:C,D:],D holds

( b_{4} 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_{4} . (x,y1)),(b_{4} . (x,y2))] in R );

for C, D being non empty set

for R being Relation

for b

( b

for y1, y2 being Element of D st [y1,y2] in R holds

[(b

scheme :: STACKS_1:sch 2

LambdaD2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( object , object ) -> Element of F_{3}() } :

LambdaD2{ F

ex M being Function of [:F_{1}(),F_{2}():],F_{3}() st

for i being Element of F_{1}()

for j being Element of F_{2}() holds M . (i,j) = F_{4}(i,j)

for i being Element of F

for j being Element of F

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 ;

ex b_{1} 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_{1} . (x,y) = Class (R,(b . (x,y1)))

for b_{1}, b_{2} 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_{1} . (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_{2} . (x,y) = Class (R,(b . (x,y1))) ) holds

b_{1} = b_{2}

end;
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 :Def2: :: STACKS_1:def 2

for x, y, y1 being set st x in C & y in Class R & y1 in y holds

it . (x,y) = Class (R,(b . (x,y1)));

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

ex b

for x, y, y1 being set st x in C & y in Class R & y1 in y holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being Function of [:C,(Class R):],(Class R) holds

( b_{5} = b /\/ R iff for x, y, y1 being set st x in C & y in Class R & y1 in y holds

b_{5} . (x,y) = Class (R,(b . (x,y1))) );

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

( b

b

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

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

definition

attr c_{1} is strict ;

struct StackSystem -> 2-sorted ;

aggr StackSystem(# carrier, carrier', s_empty, s_push, s_pop, s_top #) -> StackSystem ;

sel s_empty c_{1} -> Subset of the carrier' of c_{1};

sel s_push c_{1} -> Function of [: the carrier of c_{1}, the carrier' of c_{1}:], the carrier' of c_{1};

sel s_pop c_{1} -> Function of the carrier' of c_{1}, the carrier' of c_{1};

sel s_top c_{1} -> Function of the carrier' of c_{1}, the carrier of c_{1};

end;
struct StackSystem -> 2-sorted ;

aggr StackSystem(# carrier, carrier', s_empty, s_push, s_pop, s_top #) -> StackSystem ;

sel s_empty c

sel s_push c

sel s_pop c

sel s_top c

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;

coherence

not StackSystem(# a1,a2,a3,a4,a5,a6 #) is empty ;

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

coherence

not StackSystem(# a1,a2,a3,a4,a5,a6 #) is empty ;

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;

coherence

not StackSystem(# a1,a2,a3,a4,a5,a6 #) is void ;

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

coherence

not StackSystem(# a1,a2,a3,a4,a5,a6 #) is void ;

registration

existence

ex b_{1} being StackSystem st

( not b_{1} is empty & not b_{1} is void & b_{1} is strict )

end;
ex b

( not b

proof end;

definition
end;

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

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;

coherence

the s_pop of X . s is stack of X ;

coherence

the s_top of X . s is Element of X ;

end;
let s be stack of X;

coherence

the s_pop of X . s is stack of X ;

coherence

the s_top of X . s is Element of X ;

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

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;

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;

coherence

the s_push of X . (e,s) is stack of X ;

end;
let s be stack of X;

let e be Element of X;

coherence

the s_push of X . (e,s) is stack of X ;

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

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 ;

ex b_{1} being non empty non void strict StackSystem st

( the carrier of b_{1} = A & the carrier' of b_{1} = A * & ( for s being stack of b_{1} 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_{1} & pop s = {} ) ) & ( for e being Element of b_{1} holds push (e,s) = <*e*> ^ g ) ) ) ) ) )

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

b_{1} = b_{2}

end;
func StandardStackSystem A -> non empty non void strict StackSystem means :Def7: :: STACKS_1:def 7

( the carrier of it = A & the carrier' of it = A * & ( for s being stack of it holds

( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds

( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of it & pop s = {} ) ) & ( for e being Element of it holds push (e,s) = <*e*> ^ g ) ) ) ) ) );

existence ( 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 ) ) ) ) ) );

ex b

( the carrier of b

( ( 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

proof end;

uniqueness for b

( ( 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

( ( 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

b

proof end;

:: deftheorem Def7 defines StandardStackSystem STACKS_1:def 7 :

for A being non empty set

for b_{2} being non empty non void strict StackSystem holds

( b_{2} = StandardStackSystem A iff ( the carrier of b_{2} = A & the carrier' of b_{2} = A * & ( for s being stack of b_{2} 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_{2} & pop s = {} ) ) & ( for e being Element of b_{2} holds push (e,s) = <*e*> ^ g ) ) ) ) ) ) );

for A being non empty set

for b

( b

( ( 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

registration
end;

registration

let A be non empty set ;

coherence

for b_{1} being stack of (StandardStackSystem A) holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

definition

let X be non empty non void StackSystem ;

end;
attr X is pop-finite means :Def8: :: STACKS_1:def 8

for f being sequence of 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 ) );

for f being sequence of 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 :Def9: :: STACKS_1:def 9

for s being stack of X st not emp s holds

s = push ((top s),(pop s));

for s being stack of X st not emp s holds

s = push ((top s),(pop s));

attr X 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));

for s being stack of X

for e being Element of X holds e = top (push (e,s));

attr X 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));

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 :Def12: :: STACKS_1:def 12

for s being stack of X

for e being Element of X holds not emp push (e,s);

for s being stack of X

for e being Element of X holds not emp push (e,s);

:: 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 sequence of 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 ) ) );

for X being non empty non void StackSystem holds

( X is pop-finite iff for f being sequence of the carrier' of X ex i being Nat ex s being stack of X st

( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) );

:: deftheorem Def9 defines push-pop STACKS_1:def 9 :

for X being non empty non void StackSystem holds

( X is push-pop iff for s being stack of X st not emp s holds

s = push ((top s),(pop s)) );

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

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

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

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 ;

coherence

StandardStackSystem A is pop-finite

StandardStackSystem A is push-pop

StandardStackSystem A is top-push

StandardStackSystem A is pop-push

StandardStackSystem A is push-non-empty

end;
coherence

StandardStackSystem A is pop-finite

proof end;

coherence StandardStackSystem A is push-pop

proof end;

coherence StandardStackSystem A is top-push

proof end;

coherence StandardStackSystem A is pop-push

proof end;

coherence StandardStackSystem A is push-non-empty

proof end;

registration

ex b_{1} being non empty non void StackSystem st

( b_{1} is pop-finite & b_{1} is push-pop & b_{1} is top-push & b_{1} is pop-push & b_{1} is push-non-empty & b_{1} is strict )
end;

cluster non empty non void V70() strict pop-finite push-pop top-push pop-push push-non-empty for StackSystem ;

existence ex b

( b

proof end;

definition

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

end;
registration

let X be non empty non void pop-finite StackSystem ;

coherence

not the s_empty of X is empty

end;
coherence

not the s_empty of X is empty

proof end;

theorem Th3: :: STACKS_1:3

for X being non empty non void StackSystem

for s1, s2 being stack of X

for e1, e2 being Element of X st X is top-push & X is pop-push & push (e1,s1) = push (e2,s2) holds

( e1 = e2 & s1 = s2 )

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

for X being non empty non void StackSystem

for s1, s2 being stack of X st X is push-pop & not emp s1 & not emp s2 & pop s1 = pop s2 & top s1 = top s2 holds

s1 = s2

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;

scheme :: STACKS_1:sch 3

INDsch{ F_{1}() -> StackAlgebra, F_{2}() -> stack of F_{1}(), P_{1}[ set ] } :

provided

INDsch{ F

provided

A1:
for s being stack of F_{1}() st emp s holds

P_{1}[s]
and

A2: for s being stack of F_{1}()

for e being Element of F_{1}() st P_{1}[s] holds

P_{1}[ push (e,s)]

P

A2: for s being stack of F

for e being Element of F

P

proof end;

scheme :: STACKS_1:sch 4

EXsch{ F_{1}() -> StackAlgebra, F_{2}() -> stack of F_{1}(), F_{3}() -> non empty set , F_{4}() -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}() } :

EXsch{ F

ex a being Element of F_{3}() ex F being Function of the carrier' of F_{1}(),F_{3}() st

( a = F . F_{2}() & ( for s1 being stack of F_{1}() st emp s1 holds

F . s1 = F_{4}() ) & ( for s1 being stack of F_{1}()

for e being Element of F_{1}() holds F . (push (e,s1)) = F_{5}(e,(F . s1)) ) )

( a = F . F

F . s1 = F

for e being Element of F

proof end;

scheme :: STACKS_1:sch 5

UNIQsch{ F_{1}() -> StackAlgebra, F_{2}() -> stack of F_{1}(), F_{3}() -> non empty set , F_{4}() -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}() } :

UNIQsch{ F

for a1, a2 being Element of F_{3}() st ex F being Function of the carrier' of F_{1}(),F_{3}() st

( a1 = F . F_{2}() & ( for s1 being stack of F_{1}() st emp s1 holds

F . s1 = F_{4}() ) & ( for s1 being stack of F_{1}()

for e being Element of F_{1}() holds F . (push (e,s1)) = F_{5}(e,(F . s1)) ) ) & ex F being Function of the carrier' of F_{1}(),F_{3}() st

( a2 = F . F_{2}() & ( for s1 being stack of F_{1}() st emp s1 holds

F . s1 = F_{4}() ) & ( for s1 being stack of F_{1}()

for e being Element of F_{1}() holds F . (push (e,s1)) = F_{5}(e,(F . s1)) ) ) holds

a1 = a2

( a1 = F . F

F . s1 = F

for e being Element of F

( a2 = F . F

F . s1 = F

for e being Element of F

a1 = a2

proof end;

definition

let X be StackAlgebra;

let s be stack of X;

ex b_{1} being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st

( b_{1} = 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) ) )

for b_{1}, b_{2} being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st

( b_{1} = 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_{2} = 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_{1} = b_{2}

end;
let s be stack of X;

func |.s.| -> Element of the carrier of X * means :Def13: :: STACKS_1:def 13

ex F being Function of the carrier' of X,( the carrier of X *) st

( it = F . s & ( for s1 being stack of X st emp s1 holds

F . s1 = {} ) & ( for s1 being stack of X

for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) );

existence ex 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) ) );

ex b

( b

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

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 . s1 = {} ) & ( for s1 being stack of X

for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) holds

b

proof end;

:: deftheorem Def13 defines |. STACKS_1:def 13 :

for X being StackAlgebra

for s being stack of X

for b_{3} being Element of the carrier of X * holds

( b_{3} = |.s.| iff ex F being Function of the carrier' of X,( the carrier of X *) st

( b_{3} = 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) ) ) );

for X being StackAlgebra

for s being stack of X

for b

( b

( b

F . s1 = {} ) & ( for s1 being stack of X

for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) );

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

for s being stack of X st not emp s holds

|.s.| = <*(top s)*> ^ |.(pop s).|

proof end;

theorem Th8: :: STACKS_1:8

for X being StackAlgebra

for s being stack of X

for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|

for s being stack of X

for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|

proof end;

theorem Th12: :: STACKS_1:12

for X being StackAlgebra

for x being Element of the carrier of X * ex s being stack of X st |.s.| = x

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;

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;
let s1, s2 be stack of X;

reflexivity

for s1 being stack of X holds |.s1.| = |.s1.| ;

symmetry

for s1, s2 being stack of X st |.s1.| = |.s2.| holds

|.s2.| = |.s1.| ;

:: deftheorem defines == STACKS_1:def 14 :

for X being StackAlgebra

for s1, s2 being stack of X holds

( s1 == s2 iff |.s1.| = |.s2.| );

for X being StackAlgebra

for s1, s2 being stack of X holds

( s1 == s2 iff |.s1.| = |.s2.| );

theorem :: STACKS_1:13

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)

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 Th17: :: STACKS_1:17

for X being StackAlgebra

for s1, s2 being stack of X st s1 == s2 & not emp s1 holds

pop s1 == pop s2

for s1, s2 being stack of X st s1 == s2 & not emp s1 holds

pop s1 == pop s2

proof end;

definition

let X be StackAlgebra;

end;
attr X is proper-for-identity means :Def15: :: STACKS_1:def 15

for s1, s2 being stack of X st s1 == s2 holds

s1 = s2;

for s1, s2 being stack of X st s1 == s2 holds

s1 = s2;

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

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

definition

let X be StackAlgebra;

ex b_{1} being Relation of the carrier' of X st

for s1, s2 being stack of X holds

( [s1,s2] in b_{1} iff s1 == s2 )

for b_{1}, b_{2} being Relation of the carrier' of X st ( for s1, s2 being stack of X holds

( [s1,s2] in b_{1} iff s1 == s2 ) ) & ( for s1, s2 being stack of X holds

( [s1,s2] in b_{2} iff s1 == s2 ) ) holds

b_{1} = b_{2}

end;
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 for s1, s2 being stack of X holds

( [s1,s2] in it iff s1 == s2 );

ex b

for s1, s2 being stack of X holds

( [s1,s2] in b

proof end;

uniqueness for b

( [s1,s2] in b

( [s1,s2] in b

b

proof end;

:: deftheorem Def16 defines ==_ STACKS_1:def 16 :

for X being StackAlgebra

for b_{2} being Relation of the carrier' of X holds

( b_{2} = ==_ X iff for s1, s2 being stack of X holds

( [s1,s2] in b_{2} iff s1 == s2 ) );

for X being StackAlgebra

for b

( b

( [s1,s2] in b

registration

let X be StackAlgebra;

coherence

( ==_ X is total & ==_ X is symmetric & ==_ X is transitive )

end;
coherence

( ==_ X is total & ==_ X is symmetric & ==_ X is transitive )

proof end;

definition

let X be StackAlgebra;

let s be stack of X;

ex b_{1} being Subset of the carrier' of X st

( s in b_{1} & ( for e being Element of X

for s1 being stack of X st s1 in b_{1} holds

( push (e,s1) in b_{1} & ( not emp s1 implies pop s1 in b_{1} ) ) ) & ( 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_{1} c= A ) )

for b_{1}, b_{2} being Subset of the carrier' of X st s in b_{1} & ( for e being Element of X

for s1 being stack of X st s1 in b_{1} holds

( push (e,s1) in b_{1} & ( not emp s1 implies pop s1 in b_{1} ) ) ) & ( 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_{1} c= A ) & s in b_{2} & ( for e being Element of X

for s1 being stack of X st s1 in b_{2} holds

( push (e,s1) in b_{2} & ( not emp s1 implies pop s1 in b_{2} ) ) ) & ( 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_{2} c= A ) holds

b_{1} = b_{2}
;

end;
let s be stack of X;

func coset s -> Subset of the carrier' of X means :Def17: :: STACKS_1:def 17

( s in it & ( for e being Element of X

for s1 being stack of X st s1 in it holds

( push (e,s1) in it & ( not emp s1 implies pop s1 in it ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X

for s1 being stack of X st s1 in A holds

( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds

it c= A ) );

existence ( 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 ) );

ex b

( s in b

for s1 being stack of X st s1 in b

( push (e,s1) in b

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

proof end;

uniqueness for b

for s1 being stack of X st s1 in b

( push (e,s1) in b

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

for s1 being stack of X st s1 in b

( push (e,s1) in b

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

b

:: deftheorem Def17 defines coset STACKS_1:def 17 :

for X being StackAlgebra

for s being stack of X

for b_{3} being Subset of the carrier' of X holds

( b_{3} = coset s iff ( s in b_{3} & ( for e being Element of X

for s1 being stack of X st s1 in b_{3} holds

( push (e,s1) in b_{3} & ( not emp s1 implies pop s1 in b_{3} ) ) ) & ( 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_{3} c= A ) ) );

for X being StackAlgebra

for s being stack of X

for b

( b

for s1 being stack of X st s1 in b

( push (e,s1) in b

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

theorem Th20: :: STACKS_1:20

for X being StackAlgebra

for s, s1 being stack of X

for e being Element of X holds

( ( push (e,s) in coset s1 implies s in coset s1 ) & ( not emp s & pop s in coset s1 implies s in coset s1 ) )

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

for X being StackAlgebra

for s being stack of X

for e being Element of X holds

( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )

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

for X being StackAlgebra

for s being stack of X ex s1 being stack of X st

( emp s1 & s1 in coset s )

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;

ex b_{1} being RedSequence of R st b_{1} is A -valued

end;
let R be Relation of A;

cluster Relation-like NAT -defined A -valued Function-like non empty V49() FinSequence-like FinSubsequence-like for RedSequence of R;

existence ex b

proof end;

definition

let X be StackAlgebra;

ex b_{1} being Relation of the carrier' of X st

for s1, s2 being stack of X holds

( [s1,s2] in b_{1} iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) )

for b_{1}, b_{2} being Relation of the carrier' of X st ( for s1, s2 being stack of X holds

( [s1,s2] in b_{1} 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_{2} iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) holds

b_{1} = b_{2}

end;
func ConstructionRed X -> Relation of the carrier' of X means :Def18: :: STACKS_1:def 18

for s1, s2 being stack of X holds

( [s1,s2] in it iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) );

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

ex b

for s1, s2 being stack of X holds

( [s1,s2] in b

proof end;

uniqueness for b

( [s1,s2] in b

( [s1,s2] in b

b

proof end;

:: deftheorem Def18 defines ConstructionRed STACKS_1:def 18 :

for X being StackAlgebra

for b_{2} being Relation of the carrier' of X holds

( b_{2} = ConstructionRed X iff for s1, s2 being stack of X holds

( [s1,s2] in b_{2} iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) );

for X being StackAlgebra

for b

( b

( [s1,s2] in b

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 )

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_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> Relation of F_{1}(), P_{1}[ set ] } :

provided

PathIND{ F

provided

A1:
P_{1}[F_{2}()]
and

A2: F_{4}() reduces F_{2}(),F_{3}()
and

A3: for x, y being Element of F_{1}() st F_{4}() reduces F_{2}(),x & [x,y] in F_{4}() & P_{1}[x] holds

P_{1}[y]

A2: F

A3: for x, y being Element of F

P

proof end;

theorem Th24: :: STACKS_1:24

for X being StackAlgebra

for s being stack of X

for t being RedSequence of ConstructionRed X st s = t . 1 holds

rng t c= coset s

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

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;

ex b_{1} being stack of X st

( emp b_{1} & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st

( t . 1 = s & t . (len t) = b_{1} & ( for i being Nat st 1 <= i & i < len t holds

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) )

for b_{1}, b_{2} being stack of X st emp b_{1} & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st

( t . 1 = s & t . (len t) = b_{1} & ( for i being Nat st 1 <= i & i < len t holds

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp b_{2} & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st

( t . 1 = s & t . (len t) = b_{2} & ( for i being Nat st 1 <= i & i < len t holds

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) holds

b_{1} = b_{2}

end;
let s be stack of X;

func core s -> stack of X means :Def19: :: STACKS_1:def 19

( emp it & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st

( t . 1 = s & t . (len t) = it & ( for i being Nat st 1 <= i & i < len t holds

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) );

existence ( 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) ) ) ) );

ex b

( emp b

( t . 1 = s & t . (len t) = b

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) )

proof end;

uniqueness for b

( t . 1 = s & t . (len t) = b

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp b

( t . 1 = s & t . (len t) = b

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) holds

b

proof end;

:: deftheorem Def19 defines core STACKS_1:def 19 :

for X being StackAlgebra

for s, b_{3} being stack of X holds

( b_{3} = core s iff ( emp b_{3} & ex t being the carrier' of b_{1} -valued RedSequence of ConstructionRed X st

( t . 1 = s & t . (len t) = b_{3} & ( for i being Nat st 1 <= i & i < len t holds

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) ) );

for X being StackAlgebra

for s, b

( b

( t . 1 = s & t . (len t) = b

( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) ) );

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

for s being stack of X

for e being Element of X holds core (push (e,s)) = core s

proof end;

theorem Th30: :: STACKS_1:30

for X being StackAlgebra

for s being stack of X

for x being Element of the carrier of X * ex s1 being stack of X st

( |.s1.| = x & s1 in coset s )

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 Th32: :: STACKS_1:32

for X being StackAlgebra

for s, s1, s2 being stack of X st s1 in coset s & s2 in coset s & |.s1.| = |.s2.| holds

s1 = s2

for s, s1, s2 being stack of X st s1 in coset s & s2 in coset s & |.s1.| = |.s2.| holds

s1 = s2

proof end;

theorem Th33: :: STACKS_1:33

for X being StackAlgebra

for s1, s2 being stack of X ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}

for s1, s2 being stack of X ex s being stack of X st (coset s1) /\ (Class ((==_ X),s2)) = {s}

proof end;

definition

let X be StackAlgebra;

for b_{1}, b_{2} being strict StackSystem st the carrier of b_{1} = the carrier of X & the carrier' of b_{1} = Class (==_ X) & the s_empty of b_{1} = { the s_empty of X} & the s_push of b_{1} = the s_push of X /\/ (==_ X) & the s_pop of b_{1} = ( 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_{1} = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) & the carrier of b_{2} = the carrier of X & the carrier' of b_{2} = Class (==_ X) & the s_empty of b_{2} = { the s_empty of X} & the s_push of b_{2} = the s_push of X /\/ (==_ X) & the s_pop of b_{2} = ( 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_{2} = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) holds

b_{1} = b_{2}

ex b_{1} being strict StackSystem st

( the carrier of b_{1} = the carrier of X & the carrier' of b_{1} = Class (==_ X) & the s_empty of b_{1} = { the s_empty of X} & the s_push of b_{1} = the s_push of X /\/ (==_ X) & the s_pop of b_{1} = ( 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_{1} = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) )

end;
func X /== -> strict StackSystem means :Def20: :: STACKS_1:def 20

( the carrier of it = the carrier of X & the carrier' of it = Class (==_ X) & the s_empty of it = { the s_empty of X} & the s_push of it = the s_push of X /\/ (==_ X) & the s_pop of it = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of (Class (==_ X)) holds the s_top of it = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) );

uniqueness ( 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) ) );

for b

b

proof end;

existence ex b

( the carrier of b

proof end;

:: deftheorem Def20 defines /== STACKS_1:def 20 :

for X being StackAlgebra

for b_{2} being strict StackSystem holds

( b_{2} = X /== iff ( the carrier of b_{2} = the carrier of X & the carrier' of b_{2} = Class (==_ X) & the s_empty of b_{2} = { the s_empty of X} & the s_push of b_{2} = the s_push of X /\/ (==_ X) & the s_pop of b_{2} = ( 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_{2} = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) ) );

for X being StackAlgebra

for b

( b

registration
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)

for S being stack of (X /==) ex s being stack of X st S = Class ((==_ X),s)

proof end;

theorem Th36: :: STACKS_1:36

for X being StackAlgebra

for s being stack of X

for S being stack of (X /==) st S = Class ((==_ X),s) holds

( emp s iff emp S )

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 Th38: :: STACKS_1:38

for X being StackAlgebra

for s being stack of X

for e being Element of X

for S being stack of (X /==)

for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds

( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )

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 Th39: :: STACKS_1:39

for X being StackAlgebra

for s being stack of X

for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds

( pop s in pop S & Class ((==_ X),(pop s)) = pop S )

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 Th40: :: STACKS_1:40

for X being StackAlgebra

for s being stack of X

for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds

top S = top s

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;

coherence

X /== is pop-finite

X /== is push-pop

X /== is top-push

X /== is pop-push

X /== is push-non-empty

end;
coherence

X /== is pop-finite

proof end;

coherence X /== is push-pop

proof end;

coherence X /== is top-push

proof end;

coherence X /== is pop-push

proof end;

coherence X /== is push-non-empty

proof 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.|

for s being stack of X

for S being stack of (X /==) st S = Class ((==_ X),s) holds

|.S.| = |.s.|

proof end;

registration

ex b_{1} being StackAlgebra st b_{1} is proper-for-identity
end;

cluster non empty non void V70() pop-finite push-pop top-push pop-push push-non-empty proper-for-identity for StackAlgebra;

existence ex b

proof end;

definition

let X1, X2 be StackAlgebra;

let F, G be Function;

end;
let F, G be Function;

pred F,G form_isomorphism_between X1,X2 means :: 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)) ) ) ) );

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

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

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 :: STACKS_1:42

for X being StackAlgebra holds id the carrier of X, id the carrier' of X form_isomorphism_between X,X ;

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

for F, G being Function st F,G form_isomorphism_between X1,X2 holds

F " ,G " form_isomorphism_between X2,X1

proof end;

theorem Th44: :: STACKS_1:44

for X1, X2, X3 being StackAlgebra

for F1, F2, G1, 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

for F1, F2, G1, 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 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.|

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;

for X1 being StackAlgebra ex F, G being Function st F,G form_isomorphism_between X1,X1

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

end;
pred X1,X2 are_isomorphic means :: STACKS_1:def 22

ex F, G being Function st F,G form_isomorphism_between X1,X2;

reflexivity ex F, G being Function st F,G form_isomorphism_between X1,X2;

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;

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

for X1, X2 being StackAlgebra holds

( X1,X2 are_isomorphic iff ex F, G being Function st F,G form_isomorphism_between X1,X2 );

theorem :: STACKS_1:46

for X1, X2, X3 being StackAlgebra st X1,X2 are_isomorphic & X2,X3 are_isomorphic holds

X1,X3 are_isomorphic

X1,X3 are_isomorphic

proof end;

theorem :: STACKS_1:47

for X1, X2 being StackAlgebra st X1,X2 are_isomorphic & X1 is proper-for-identity holds

X2 is proper-for-identity

X2 is proper-for-identity

proof end;

theorem Th48: :: STACKS_1:48

for X being proper-for-identity StackAlgebra ex G being Function st

( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )

( ( 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:49

for X being proper-for-identity StackAlgebra holds X, StandardStackSystem the carrier of X are_isomorphic

proof end;