stacks_1.miz
begin
reserve i,j for
Nat;
reserve x,y for
set;
definition
let A be
set;
let s1,s2 be
FinSequence of A;
:: original:
^
redefine
func s1
^ s2 ->
Element of (A
* ) ;
coherence
proof
(s1
^ s2) is
FinSequence of A;
hence thesis by
FINSEQ_1:def 11;
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
proof
(
rng (
Del (s,i)))
c= (
rng s) & (
rng s)
c= A by
FINSEQ_3: 106;
then (
rng (
Del (s,i)))
c= A;
then (
Del (s,i)) is
FinSequence of A by
FINSEQ_1:def 4;
hence thesis by
FINSEQ_1:def 11;
end;
end
theorem ::
STACKS_1:1
Th1: (
Del (
{} ,i))
=
{}
proof
(
dom (
Del (
{} ,i)))
c= (
dom
{} ) by
WSIERP_1: 39;
hence thesis;
end;
scheme ::
STACKS_1:sch1
IndSeqD { D() -> non
empty
set , P[
set] } :
for p be
FinSequence of D() holds P[p]
provided
A1: P[(
<*> D())]
and
A2: for p be
FinSequence of D() holds for x be
Element of D() st P[p] holds P[(
<*x*>
^ p)];
defpred
R[
set] means for p be
FinSequence of D() st (
len p)
= $1 holds P[p];
A3: for i st
R[i] holds
R[(i
+ 1)]
proof
let i such that
A4: for p be
FinSequence of D() st (
len p)
= i holds P[p];
let p be
FinSequence of D();
assume
A5: (
len p)
= (i
+ 1);
then p
<>
{} ;
then
consider q be
FinSequence of D(), x be
Element of D() such that
A6: p
= (
<*x*>
^ q) by
FINSEQ_2: 130;
(
len p)
= ((
len q)
+ 1) by
A6,
FINSEQ_5: 8;
hence thesis by
A2,
A4,
A5,
A6;
end;
let p be
FinSequence of D();
A7: (
len p)
= (
len p);
A8:
R[
0 ]
proof
let p be
FinSequence of D();
assume (
len p)
=
0 ;
then p
= (
<*> D());
hence thesis by
A1;
end;
for i holds
R[i] from
NAT_1:sch 2(
A8,
A3);
hence thesis by
A7;
end;
definition
let C,D be non
empty
set;
let R be
Relation;
::
STACKS_1:def1
mode
BinOp of C,D,R ->
Function of
[:C, D:], D means
:
Def1: for x be
Element of C, y1,y2 be
Element of D st
[y1, y2]
in R holds
[(it
. (x,y1)), (it
. (x,y2))]
in R;
existence
proof
take f = (
pr2 (C,D));
let x be
Element of C, y1,y2 be
Element of D;
(f
. (x,y1))
= y1 by
FUNCT_3:def 5;
hence thesis by
FUNCT_3:def 5;
end;
end
scheme ::
STACKS_1:sch2
LambdaD2 { A,B,C() -> non
empty
set , F(
object,
object) ->
Element of C() } :
ex M be
Function of
[:A(), B():], C() st for i be
Element of A(), j be
Element of B() holds (M
. (i,j))
= F(i,j);
consider M be
ManySortedSet of
[:A(), B():] such that
A1: for i be
Element of A(), j be
Element of B() holds (M
. (i,j))
= F(i,j) from
ALTCAT_1:sch 2;
A2: (
dom M)
=
[:A(), B():] by
PARTFUN1:def 2;
(
rng M)
c= C()
proof
let y be
object;
assume y
in (
rng M);
then
consider x be
object such that
A3: x
in (
dom M) & y
= (M
. x) by
FUNCT_1:def 3;
consider x1,x2 be
object such that
A4: x1
in A() & x2
in B() & x
=
[x1, x2] by
A3,
ZFMISC_1:def 2;
y
= (M
. (x1,x2)) by
A3,
A4
.= F(x1,x2) by
A1,
A4;
hence thesis;
end;
then
reconsider M as
Function of
[:A(), B():], C() by
A2,
FUNCT_2: 2;
take M;
thus thesis by
A1;
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;
::
STACKS_1:def2
func b
/\/ R ->
Function of
[:C, (
Class R):], (
Class R) means
:
Def2: for x,y,y1 be
set st x
in C & y
in (
Class R) & y1
in y holds (it
. (x,y))
= (
Class (R,(b
. (x,y1))));
existence
proof
for X be
set st X
in (
Class R) holds X
<>
{} ;
then
consider g be
Function such that
A2: (
dom g)
= (
Class R) and
A3: for X be
set st X
in (
Class R) holds (g
. X)
in X by
FUNCT_1: 111;
A4: (
rng g)
c= D
proof
let x be
object;
assume x
in (
rng g);
then
consider y be
object such that
A5: y
in (
dom g) and
A6: x
= (g
. y) by
FUNCT_1:def 3;
reconsider y as
set by
TARSKI: 1;
x
in y by
A2,
A3,
A5,
A6;
hence thesis by
A2,
A5;
end;
deffunc
F(
Element of D) = (
EqClass (R,$1));
consider f be
Function of D, (
Class R) such that
A7: for x be
Element of D holds (f
. x)
=
F(x) from
FUNCT_2:sch 4;
reconsider g as
Function of (
Class R), D by
A2,
A4,
FUNCT_2:def 1,
RELSET_1: 4;
deffunc
F(
Element of C,
Element of (
Class R)) = (f
. (b
. ($1,(g
. $2))));
consider bR be
Function of
[:C, (
Class R):], (
Class R) such that
A8: for x be
Element of C, y be
Element of (
Class R) holds (bR
. (x,y))
=
F(x,y) from
LambdaD2;
take bR;
let x,y,y1 be
set;
assume that
A9: x
in C and
A10: y
in (
Class R) and
A11: y1
in y;
reconsider x9 = x as
Element of C by
A9;
reconsider y9 = y as
Element of (
Class R) by
A10;
reconsider y19 = y1 as
Element of D by
A10,
A11;
A12: ex y2 be
object st y2
in D & y9
= (
Class (R,y2)) by
EQREL_1:def 3;
(g
. y9)
in y by
A3;
then
[(g
. y9), y19]
in R by
A11,
A12,
EQREL_1: 22;
then
[(b
. (x9,(g
. y9))), (b
. (x9,y19))]
in R by
A1,
Def1;
then
A13: (b
. (x9,(g
. y9)))
in (
EqClass (R,(b
. (x9,y19)))) by
EQREL_1: 19;
A14: (f
. (b
. (x9,(g
. y9))))
= (
EqClass (R,(b
. (x9,(g
. y9))))) by
A7;
(bR
. (x9,y9))
= (f
. (b
. (x9,(g
. y9)))) by
A8;
hence thesis by
A13,
A14,
EQREL_1: 23;
end;
uniqueness
proof
let b1,b2 be
Function of
[:C, (
Class R):], (
Class R) such that
A15: for x,y,y1 be
set st x
in C & y
in (
Class R) & y1
in y holds (b1
. (x,y))
= (
Class (R,(b
. (x,y1)))) and
A16: for x,y,y1 be
set st x
in C & y
in (
Class R) & y1
in y holds (b2
. (x,y))
= (
Class (R,(b
. (x,y1))));
now
let x be
Element of C, y be
Element of (
Class R);
consider y1 be
object such that
A17: y1
in D and
A18: y
= (
Class (R,y1)) by
EQREL_1:def 3;
(b1
. (x,y))
= (
Class (R,(b
. (x,y1)))) by
A15,
A17,
A18,
EQREL_1: 20;
hence (b1
. (x,y))
= (b2
. (x,y)) by
A16,
A17,
A18,
EQREL_1: 20;
end;
hence thesis;
end;
end
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
proof
per cases ;
suppose D
=
{} ;
then
A1: g
=
{} ;
thus thesis by
A1;
end;
suppose
A2: D
<>
{} ;
A3: (
dom (f
+* g))
= ((
dom f)
\/ (
dom g)) by
FUNCT_4:def 1
.= (A
\/ (
dom g)) by
FUNCT_2:def 1
.= (A
\/ C) by
A2,
FUNCT_2:def 1
.= A by
XBOOLE_1: 12;
A4: (
rng (f
+* g))
c= ((
rng f)
\/ (
rng g)) by
FUNCT_4: 17;
((
rng f)
\/ (
rng g))
c= (B
\/ D) & (B
\/ D)
= B by
XBOOLE_1: 12,
XBOOLE_1: 13;
hence thesis by
A3,
A4,
FUNCT_2: 2,
XBOOLE_1: 1;
end;
end;
end
begin
definition
struct (
2-sorted)
StackSystem
(# the
carrier ->
set,
the
carrier' ->
set,
the
s_empty ->
Subset of the carrier',
the
s_push ->
Function of
[: the carrier, the carrier':], the carrier',
the
s_pop ->
Function of the carrier', the carrier',
the
s_top ->
Function of the carrier', the carrier #)
attr strict
strict;
end
registration
let a1 be non
empty
set, a2 be
set, a3 be
Subset of a2, a4 be
Function of
[:a1, a2:], a2, a5 be
Function of a2, a2, a6 be
Function of a2, a1;
cluster
StackSystem (# a1, a2, a3, a4, a5, a6 #) -> non
empty;
coherence ;
end
registration
let a1 be
set, a2 be non
empty
set, a3 be
Subset of a2, a4 be
Function of
[:a1, a2:], a2, a5 be
Function of a2, a2, a6 be
Function of a2, a1;
cluster
StackSystem (# a1, a2, a3, a4, a5, a6 #) -> non
void;
coherence ;
end
registration
cluster non
empty non
void
strict for
StackSystem;
existence
proof
set a1 = the non
empty
set, a2 = a1;
set a3 = the
Subset of a2, a4 = the
Function of
[:a1, a2:], a2, a5 = the
Function of a2, a2, a6 = the
Function of a2, a1;
take
StackSystem (# a1, a2, a3, a4, a5, a6 #);
thus thesis;
end;
end
definition
let X be
StackSystem;
mode
stack of X is
Element of the
carrier' of X;
end
definition
let X be
StackSystem;
let s be
stack of X;
::
STACKS_1:def3
pred
emp s means s
in the
s_empty of X;
end
definition
let X be non
void
StackSystem;
let s be
stack of X;
::
STACKS_1:def4
func
pop s ->
stack of X equals (the
s_pop of X
. s);
coherence ;
::
STACKS_1:def5
func
top s ->
Element of X equals (the
s_top of X
. s);
coherence ;
end
definition
let X be non
empty non
void
StackSystem;
let s be
stack of X;
let e be
Element of X;
::
STACKS_1:def6
func
push (e,s) ->
stack of X equals (the
s_push of X
. (e,s));
coherence ;
end
definition
let A be non
empty
set;
::
STACKS_1:def7
func
StandardStackSystem A -> non
empty non
void
strict
StackSystem means
:
Def7: the
carrier of it
= A & the
carrier' of it
= (A
* ) & for s be
stack of it holds (
emp s iff s is
empty) & for g be
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 be
Element of it holds (
push (e,s))
= (
<*e*>
^ g);
existence
proof
reconsider s0 = (
<*> A) as
Element of (A
* ) by
FINSEQ_1:def 11;
set E =
{s0};
deffunc
F(
Element of A,
Element of (A
* )) = (
<*$1*>
^ $2);
deffunc
G(
Element of (A
* )) = (
Del ($1,1));
deffunc
H(
Element of (A
* )) = (
IFEQ ($1,
{} , the
Element of A,($1
/. 1)));
consider psh be
Function of
[:A, (A
* ):], (A
* ) such that
A1: for a be
Element of A holds for s be
Element of (A
* ) holds (psh
. (a,s))
=
F(a,s) from
BINOP_1:sch 4;
consider pp be
Function of (A
* ), (A
* ) such that
A2: for s be
Element of (A
* ) holds (pp
. s)
=
G(s) from
FUNCT_2:sch 4;
consider tp be
Function of (A
* ), A such that
A3: for s be
Element of (A
* ) holds (tp
. s)
=
H(s) from
FUNCT_2:sch 4;
take X =
StackSystem (# A, (A
* ), E, psh, pp, tp #);
thus the
carrier of X
= A & the
carrier' of X
= (A
* );
let s be
stack of X;
thus
A4:
emp s iff s is
empty by
TARSKI:def 1;
let g be
FinSequence;
assume
A5: g
= s;
then
reconsider h = g as
Element of (A
* );
hereby
assume
A6: not
emp s;
then
A7: 1
in (
dom h) by
A4,
A5,
FINSEQ_5: 6;
thus (
top s)
= (
IFEQ (s,
{} , the
Element of A,(h
/. 1))) by
A3,
A5
.= (h
/. 1) by
A4,
A6,
FUNCOP_1:def 8
.= (g
. 1) by
A7,
PARTFUN1:def 6;
thus (
pop s)
= (
Del (g,1)) by
A5,
A2;
end;
hereby
assume
A8:
emp s;
thus (
top s)
= (
IFEQ (s,
{} , the
Element of A,(h
/. 1))) by
A3,
A5
.= the
Element of X by
A4,
A8,
FUNCOP_1:def 8;
thus (
pop s)
= (
Del (g,1)) by
A5,
A2
.=
{} by
A4,
A5,
A8,
Th1;
end;
let e be
Element of X;
thus (
push (e,s))
= (
<*e*>
^ g) by
A1,
A5;
end;
uniqueness
proof
let X1,X2 be non
empty non
void
strict
StackSystem such that
A9: the
carrier of X1
= A and
A10: the
carrier' of X1
= (A
* ) and
A11: for s be
stack of X1 holds (
emp s iff s is
empty) & for g be
FinSequence st g
= s holds ( not
emp s implies (
top s)
= (g
. 1) & (
pop s)
= (
Del (g,1))) & (
emp s implies (
top s)
= the
Element of X1 & (
pop s)
=
{} ) & for e be
Element of X1 holds (
push (e,s))
= (
<*e*>
^ g) and
A12: the
carrier of X2
= A and
A13: the
carrier' of X2
= (A
* ) and
A14: for s be
stack of X2 holds (
emp s iff s is
empty) & for g be
FinSequence st g
= s holds ( not
emp s implies (
top s)
= (g
. 1) & (
pop s)
= (
Del (g,1))) & (
emp s implies (
top s)
= the
Element of X2 & (
pop s)
=
{} ) & for e be
Element of X2 holds (
push (e,s))
= (
<*e*>
^ g);
now
let x be
Element of A;
reconsider e1 = x as
Element of X1 by
A9;
reconsider e2 = x as
Element of X2 by
A12;
let y be
Element of (A
* );
reconsider s1 = y as
stack of X1 by
A10;
reconsider s2 = y as
stack of X2 by
A13;
thus (the
s_push of X1
. (x,y))
= (
push (e1,s1))
.= (
<*x*>
^ y) by
A11
.= (
push (e2,s2)) by
A14
.= (the
s_push of X2
. (x,y));
end;
then
A15: the
s_push of X1
= the
s_push of X2 by
A9,
A10,
A12,
A13,
BINOP_1: 2;
now
let x be
Element of (A
* );
reconsider s1 = x as
stack of X1 by
A10;
reconsider s2 = x as
stack of X2 by
A13;
per cases ;
suppose
A16: not
emp s1;
then s1 is non
empty by
A11;
then
A17: not
emp s2 by
A14;
thus (the
s_pop of X1
. x)
= (
pop s1)
.= (
Del (x,1)) by
A16,
A11
.= (
pop s2) by
A17,
A14
.= (the
s_pop of X2
. x);
end;
suppose
A18:
emp s1;
then s1 is
empty by
A11;
then
A19:
emp s2 by
A14;
thus (the
s_pop of X1
. x)
= (
pop s1)
.=
{} by
A18,
A11
.= (
pop s2) by
A19,
A14
.= (the
s_pop of X2
. x);
end;
end;
then
A20: the
s_pop of X1
= the
s_pop of X2 by
A10,
A13;
A21:
now
let x be
Element of (A
* );
reconsider s1 = x as
stack of X1 by
A10;
reconsider s2 = x as
stack of X2 by
A13;
per cases ;
suppose
A22: not
emp s1;
then s1 is non
empty by
A11;
then
A23: not
emp s2 by
A14;
thus (the
s_top of X1
. x)
= (
top s1)
.= (x
. 1) by
A22,
A11
.= (
top s2) by
A23,
A14
.= (the
s_top of X2
. x);
end;
suppose
A24:
emp s1;
then s1 is
empty by
A11;
then
A25:
emp s2 by
A14;
thus (the
s_top of X1
. x)
= (
top s1)
.= the
Element of A by
A9,
A24,
A11
.= (
top s2) by
A12,
A25,
A14
.= (the
s_top of X2
. x);
end;
end;
the
s_empty of X1
= the
s_empty of X2
proof
thus the
s_empty of X1
c= the
s_empty of X2
proof
let x be
object;
assume
A26: x
in the
s_empty of X1;
then
reconsider s1 = x as
stack of X1;
reconsider s2 = s1 as
stack of X2 by
A10,
A13;
emp s1 by
A26;
then s1 is
empty by
A11;
then
emp s2 by
A14;
hence thesis;
end;
let x be
object;
assume
A27: x
in the
s_empty of X2;
then
reconsider s2 = x as
stack of X2;
reconsider s1 = s2 as
stack of X1 by
A10,
A13;
emp s2 by
A27;
then s2 is
empty by
A14;
then
emp s1 by
A11;
hence thesis;
end;
hence thesis by
A9,
A10,
A12,
A15,
A20,
A21,
FUNCT_2: 63;
end;
end
reserve A for non
empty
set;
reserve c for
Element of (
StandardStackSystem A);
reserve m for
stack of (
StandardStackSystem A);
registration
let A;
cluster the
carrier' of (
StandardStackSystem A) ->
functional;
coherence
proof
the
carrier' of (
StandardStackSystem A)
= (A
* ) by
Def7;
hence thesis;
end;
end
registration
let A;
cluster ->
FinSequence-like for
stack of (
StandardStackSystem A);
coherence
proof
the
carrier' of (
StandardStackSystem A)
= (A
* ) by
Def7;
hence thesis;
end;
end
::$Unknown
reserve X for non
empty non
void
StackSystem;
reserve s,s1,s2 for
stack of X;
reserve e,e1,e2 for
Element of X;
definition
let X;
::
STACKS_1:def8
attr X is
pop-finite means
:
Def8: for f be
sequence of the
carrier' of X holds ex i be
Nat, s st (f
. i)
= s & ( not
emp s implies (f
. (i
+ 1))
<> (
pop s));
::
STACKS_1:def9
attr X is
push-pop means
:
Def9: not
emp s implies s
= (
push ((
top s),(
pop s)));
::
STACKS_1:def10
attr X is
top-push means
:
Def10: e
= (
top (
push (e,s)));
::
STACKS_1:def11
attr X is
pop-push means
:
Def11: s
= (
pop (
push (e,s)));
::
STACKS_1:def12
attr X is
push-non-empty means
:
Def12: not
emp (
push (e,s));
end
registration
let A be non
empty
set;
cluster (
StandardStackSystem A) ->
pop-finite;
coherence
proof
set X = (
StandardStackSystem A);
let f be
sequence of the
carrier' of X such that
A1: for i be
Nat, s be
stack of X st (f
. i)
= s holds not
emp s & (f
. (i
+ 1))
= (
pop s);
reconsider g = (f
. 1) as
Element of (A
* ) by
Def7;
defpred
P[
Nat] means ex i st ex g be
Element of (A
* ) st g
= (f
. i) & $1
= (
len g);
A2: ex k be
Nat st
P[k]
proof
take k = (
len g), i = 1, g;
thus thesis;
end;
A3: for k be
Nat st k
<>
0 &
P[k] holds ex n be
Nat st n
< k &
P[n]
proof
let k be
Nat;
assume
A4: k
<>
0 ;
then
consider n0 be
Nat such that
A5: k
= (n0
+ 1) by
NAT_1: 6;
given i be
Nat, g be
Element of (A
* ) such that
A6: g
= (f
. i) & k
= (
len g);
reconsider s = g as
stack of X by
A6;
reconsider h = (
pop s) as
Element of (A
* ) by
Def7;
take n = (
len h);
A7: s is non
empty by
A4,
A6;
then not
emp s by
Def7;
then
A8: (f
. (i
+ 1))
= (
pop s) & h
= (
Del (g,1)) by
A1,
A6,
Def7;
1
in (
dom g) by
A7,
FINSEQ_5: 6;
then n0
= n by
A5,
A6,
A8,
FINSEQ_3: 109;
hence thesis by
A5,
A8,
NAT_1: 13;
end;
P[
0 ] from
NAT_1:sch 7(
A2,
A3);
then
consider i be
Nat, g be
Element of (A
* ) such that
A9: g
= (f
. i) &
0
= (
len g);
reconsider s = g as
stack of X by
A9;
g is
empty & not
emp s by
A1,
A9;
hence thesis by
Def7;
end;
cluster (
StandardStackSystem A) ->
push-pop;
coherence
proof
set X = (
StandardStackSystem A);
let s be
stack of X;
reconsider g = s as
Element of (A
* ) by
Def7;
assume
A10: not
emp s;
then
A11: s is non
empty by
Def7;
then
A12: g
= (
<*(g
. 1)*>
^ (
Del (g,1))) by
FINSEQ_5: 86;
reconsider h = (
Del (g,1)) as
stack of X by
Def7;
1
in (
dom g) by
A11,
FINSEQ_5: 6;
then (g
. 1)
in A by
FUNCT_1: 102;
then
reconsider x = (g
. 1) as
Element of X by
Def7;
thus s
= (
push (x,h)) by
A12,
Def7
.= (
push ((
top s),h)) by
A10,
Def7
.= (
push ((
top s),(
pop s))) by
A10,
Def7;
end;
cluster (
StandardStackSystem A) ->
top-push;
coherence
proof
set X = (
StandardStackSystem A);
let s be
stack of X;
let e be
Element of X;
reconsider g = s as
Element of (A
* ) by
Def7;
reconsider h = (
push (e,s)) as
Element of (A
* ) by
Def7;
A13: h
= (
<*e*>
^ g) by
Def7;
then
A14: not
emp (
push (e,s)) by
Def7;
thus e
= (h
. 1) by
A13,
FINSEQ_1: 41
.= (
top (
push (e,s))) by
A14,
Def7;
end;
cluster (
StandardStackSystem A) ->
pop-push;
coherence
proof
set X = (
StandardStackSystem A);
let s be
stack of X;
let e be
Element of X;
reconsider g = s as
Element of (A
* ) by
Def7;
reconsider h = (
push (e,s)) as
Element of (A
* ) by
Def7;
A15: h
= (
<*e*>
^ g) by
Def7;
then
A16: not
emp (
push (e,s)) by
Def7;
thus s
= (
Del ((
<*e*>
^ g),1)) by
WSIERP_1: 40
.= (
pop (
push (e,s))) by
A15,
A16,
Def7;
end;
cluster (
StandardStackSystem A) ->
push-non-empty;
coherence
proof
set X = (
StandardStackSystem A);
let s be
stack of X;
let e be
Element of X;
reconsider g = s as
Element of (A
* ) by
Def7;
(
push (e,s))
= (
<*e*>
^ g) by
Def7;
hence not
emp (
push (e,s)) by
Def7;
end;
end
registration
cluster
pop-finite
push-pop
top-push
pop-push
push-non-empty
strict for non
empty non
void
StackSystem;
existence
proof
take (
StandardStackSystem the non
empty
set);
thus thesis;
end;
end
definition
mode
StackAlgebra is
pop-finite
push-pop
top-push
pop-push
push-non-empty non
empty non
void
StackSystem;
end
theorem ::
STACKS_1:2
Th2: for X be non
empty non
void
StackSystem st X is
pop-finite holds ex s be
stack of X st
emp s
proof
let X be non
empty non
void
StackSystem such that
A1: X is
pop-finite;
set s1 = the
stack of X;
defpred
P[
set,
stack of X,
stack of X] means $3
= (
pop $2);
A2: for n be
Nat holds for x be
stack of X holds ex y be
stack of X st
P[n, x, y];
consider f be
sequence of the
carrier' of X such that
A3: (f
.
0 )
= s1 & for n be
Nat holds
P[n, (f
. n), (f
. (n
+ 1))] from
RECDEF_1:sch 2(
A2);
consider i be
Nat, s be
stack of X such that
A4: (f
. i)
= s & ( not
emp s implies (f
. (i
+ 1))
<> (
pop s)) by
A1;
take s;
thus thesis by
A3,
A4;
end;
registration
let X be
pop-finite non
empty non
void
StackSystem;
cluster the
s_empty of X -> non
empty;
coherence
proof
ex s be
stack of X st
emp s by
Th2;
hence thesis;
end;
end
theorem ::
STACKS_1:3
Th3: X is
top-push
pop-push & (
push (e1,s1))
= (
push (e2,s2)) implies e1
= e2 & s1
= s2
proof
assume X is
top-push;
then
A1: e1
= (
top (
push (e1,s1))) & e2
= (
top (
push (e2,s2)));
assume X is
pop-push;
then s1
= (
pop (
push (e1,s1))) & s2
= (
pop (
push (e2,s2)));
hence thesis by
A1;
end;
theorem ::
STACKS_1:4
X is
push-pop & not
emp s1 & not
emp s2 & (
pop s1)
= (
pop s2) & (
top s1)
= (
top s2) implies s1
= s2
proof
assume
A1: X is
push-pop;
assume not
emp s1;
then s1
= (
push ((
top s1),(
pop s1))) by
A1;
hence thesis by
A1;
end;
begin
scheme ::
STACKS_1:sch3
INDsch { X() ->
StackAlgebra , s() ->
stack of X() , P[
set] } :
P[s()]
provided
A1: for s be
stack of X() st
emp s holds P[s]
and
A2: for s be
stack of X(), e be
Element of X() st P[s] holds P[(
push (e,s))];
defpred
Q[
set,
stack of X(),
stack of X()] means $3
= (
pop $2);
A3: for n be
Nat holds for x be
stack of X() holds ex y be
stack of X() st
Q[n, x, y];
consider f be
sequence of the
carrier' of X() such that
A4: (f
.
0 )
= s() & for n be
Nat holds
Q[n, (f
. n), (f
. (n
+ 1))] from
RECDEF_1:sch 2(
A3);
consider i be
Nat, s be
stack of X() such that
A5: (f
. i)
= s & ( not
emp s implies (f
. (i
+ 1))
<> (
pop s)) by
Def8;
defpred
R[
Nat] means P[(f
. (i
-' $1))];
(i
-'
0 )
= i by
NAT_D: 40;
then
A6:
R[
0 ] by
A5,
A4,
A1;
A7:
now
let j be
Nat;
assume
A8:
R[j];
A9: (i
-' (j
+ 1))
= ((i
-' j)
-' 1) by
NAT_2: 30;
per cases ;
suppose (i
-' j)
>= 1;
then ((i
-' (j
+ 1))
+ 1)
= (i
-' j) by
A9,
XREAL_1: 235;
then (f
. (i
-' j))
= (
pop (f
. (i
-' (j
+ 1)))) by
A4;
then not
emp (f
. (i
-' (j
+ 1))) implies (f
. (i
-' (j
+ 1)))
= (
push ((
top (f
. (i
-' (j
+ 1)))),(f
. (i
-' j)))) by
Def9;
hence
R[(j
+ 1)] by
A1,
A2,
A8;
end;
suppose
A10: (i
-' j)
< (
0
+ 1);
then
A11: (i
-' j)
<=
0 by
NAT_1: 13;
A12: (i
-' j)
=
0 by
A10,
NAT_1: 13;
(i
-' (j
+ 1))
= (
0
-' 1) by
A12,
NAT_2: 30
.=
0 by
NAT_2: 8;
hence
R[(j
+ 1)] by
A8,
A11;
end;
end;
for j be
Nat holds
R[j] from
NAT_1:sch 2(
A6,
A7);
then
R[i];
hence thesis by
A4,
XREAL_1: 232;
end;
scheme ::
STACKS_1:sch4
EXsch { X() ->
StackAlgebra , s() ->
stack of X() , A() -> non
empty
set , e() ->
Element of A() , d(
set,
set) ->
Element of A() } :
ex a be
Element of A() st ex F be
Function of the
carrier' of X(), A() st a
= (F
. s()) & (for s1 be
stack of X() st
emp s1 holds (F
. s1)
= e()) & for s1 be
stack of X(), e be
Element of X() holds (F
. (
push (e,s1)))
= d(e,.);
defpred
G[
set] means (for s be
stack of X() st
emp s holds
[s, e()]
in $1) & (for s be
stack of X(), a be
Element of X(), v be
Element of A() st
[s, v]
in $1 holds
[(
push (a,s)), d(a,v)]
in $1);
consider M be
set such that
A1: x
in M iff x
in (
bool
[:the
carrier' of X(), A():]) &
G[x] from
XFAMILY:sch 1;
A2:
G[
[:the
carrier' of X(), A():]] &
[:the
carrier' of X(), A():]
in (
bool
[:the
carrier' of X(), A():]) by
ZFMISC_1:def 1;
then
A3:
[:the
carrier' of X(), A():]
in M by
A1;
reconsider M as non
empty
set by
A1,
A2;
set F = (
meet M);
reconsider F as
Subset of
[:the
carrier' of X(), A():] by
A3,
SETFAM_1: 3;
defpred
P[
stack of X()] means for y1,y2 be
object st
[$1, y1]
in F &
[$1, y2]
in F holds y1
= y2;
A4:
G[F]
proof
hereby
let s be
stack of X();
assume
emp s;
then for Y be
set st Y
in M holds
[s, e()]
in Y by
A1;
hence
[s, e()]
in F by
SETFAM_1:def 1;
end;
let s be
stack of X(), a be
Element of X(), v be
Element of A();
assume
A5:
[s, v]
in F;
now
let Y be
set;
assume Y
in M;
then
G[Y] &
[s, v]
in Y by
A5,
A1,
SETFAM_1:def 1;
hence
[(
push (a,s)), d(a,v)]
in Y;
end;
hence
[(
push (a,s)), d(a,v)]
in F by
SETFAM_1:def 1;
end;
defpred
Q[
stack of X()] means ex y be
set st
[$1, y]
in F;
A6: for s be
stack of X() st
emp s holds
Q[s]
proof
let s be
stack of X();
assume
A7:
emp s;
take y = e();
for Y be
set st Y
in M holds
[s, e()]
in Y by
A7,
A1;
hence thesis by
SETFAM_1:def 1;
end;
A8: for s be
stack of X(), e be
Element of X() st
Q[s] holds
Q[(
push (e,s))]
proof
let s be
stack of X(), e be
Element of X();
given y be
set such that
A9:
[s, y]
in F;
reconsider y as
Element of A() by
A9,
ZFMISC_1: 87;
take z = d(e,y);
now
let Y be
set;
assume
A10: Y
in M;
then
[s, y]
in Y by
A9,
SETFAM_1:def 1;
hence
[(
push (e,s)), z]
in Y by
A10,
A1;
end;
hence thesis by
SETFAM_1:def 1;
end;
A11: for s be
stack of X() st
emp s holds
P[s]
proof
let s be
stack of X();
assume
A12:
emp s;
let y1,y2 be
object;
assume
A13:
[s, y1]
in F &
[s, y2]
in F;
set Y1 = (F
\
{
[s, y1]}), Y2 = (F
\
{
[s, y2]});
A14:
now
assume
A15: y1
<> e();
G[Y1]
proof
hereby
let s1 be
stack of X();
assume
emp s1;
then
A16:
[s1, e()]
in F by
A4;
[s, y1]
<>
[s1, e()] by
A15,
XTUPLE_0: 1;
then
[s1, e()]
nin
{
[s, y1]} by
TARSKI:def 1;
hence
[s1, e()]
in Y1 by
A16,
XBOOLE_0:def 5;
end;
let s1 be
stack of X(), a be
Element of X(), v be
Element of A();
assume
[s1, v]
in Y1;
then
[s1, v]
in F by
XBOOLE_0:def 5;
then
A17:
[(
push (a,s1)), d(a,v)]
in F by
A4;
(
push (a,s1))
<> s by
A12,
Def12;
then
[s, y1]
<>
[(
push (a,s1)), d(a,v)] by
XTUPLE_0: 1;
then
[(
push (a,s1)), d(a,v)]
nin
{
[s, y1]} by
TARSKI:def 1;
hence
[(
push (a,s1)), d(a,v)]
in Y1 by
A17,
XBOOLE_0:def 5;
end;
then Y1
in M by
A1;
then F
c= Y1 by
SETFAM_1: 3;
then
[s, y1]
in Y1 &
[s, y1]
in
{
[s, y1]} by
A13,
TARSKI:def 1;
hence contradiction by
XBOOLE_0:def 5;
end;
now
assume
A18: y2
<> e();
G[Y2]
proof
hereby
let s1 be
stack of X();
assume
emp s1;
then
A19:
[s1, e()]
in F by
A4;
[s, y2]
<>
[s1, e()] by
A18,
XTUPLE_0: 1;
then
[s1, e()]
nin
{
[s, y2]} by
TARSKI:def 1;
hence
[s1, e()]
in Y2 by
A19,
XBOOLE_0:def 5;
end;
let s1 be
stack of X(), a be
Element of X(), v be
Element of A();
assume
[s1, v]
in Y2;
then
[s1, v]
in F by
XBOOLE_0:def 5;
then
A20:
[(
push (a,s1)), d(a,v)]
in F by
A4;
(
push (a,s1))
<> s by
A12,
Def12;
then
[s, y2]
<>
[(
push (a,s1)), d(a,v)] by
XTUPLE_0: 1;
then
[(
push (a,s1)), d(a,v)]
nin
{
[s, y2]} by
TARSKI:def 1;
hence
[(
push (a,s1)), d(a,v)]
in Y2 by
A20,
XBOOLE_0:def 5;
end;
then Y2
in M by
A1;
then F
c= Y2 by
SETFAM_1: 3;
then
[s, y2]
in Y2 &
[s, y2]
in
{
[s, y2]} by
A13,
TARSKI:def 1;
hence contradiction by
XBOOLE_0:def 5;
end;
hence y1
= y2 by
A14;
end;
A21: for s be
stack of X(), e be
Element of X() st
P[s] holds
P[(
push (e,s))]
proof
let s be
stack of X(), e be
Element of X();
assume
A22:
P[s];
let y1,y2 be
object;
assume
A23:
[(
push (e,s)), y1]
in F &
[(
push (e,s)), y2]
in F;
Q[s] from
INDsch(
A6,
A8);
then
consider y be
set such that
A24:
[s, y]
in F;
reconsider y as
Element of A() by
A24,
ZFMISC_1: 87;
set Y1 = (F
\
{
[(
push (e,s)), y1]}), Y2 = (F
\
{
[(
push (e,s)), y2]});
A25:
now
assume
A26: y1
<> d(e,y);
G[Y1]
proof
hereby
let s1 be
stack of X();
assume
A27:
emp s1;
then
A28:
[s1, e()]
in F by
A4;
not
emp (
push (e,s)) by
Def12;
then
[(
push (e,s)), y1]
<>
[s1, e()] by
A27,
XTUPLE_0: 1;
then
[s1, e()]
nin
{
[(
push (e,s)), y1]} by
TARSKI:def 1;
hence
[s1, e()]
in Y1 by
A28,
XBOOLE_0:def 5;
end;
let s1 be
stack of X(), a be
Element of X(), v be
Element of A();
assume
[s1, v]
in Y1;
then
A29:
[s1, v]
in F by
XBOOLE_0:def 5;
then
A30:
[(
push (a,s1)), d(a,v)]
in F by
A4;
now
assume
[(
push (e,s)), y1]
=
[(
push (a,s1)), d(a,v)];
then
A31: (
push (e,s))
= (
push (a,s1)) & y1
= d(a,v) by
XTUPLE_0: 1;
then e
= a & s
= s1 by
Th3;
hence contradiction by
A22,
A24,
A29,
A26,
A31;
end;
then
[(
push (a,s1)), d(a,v)]
nin
{
[(
push (e,s)), y1]} by
TARSKI:def 1;
hence
[(
push (a,s1)), d(a,v)]
in Y1 by
A30,
XBOOLE_0:def 5;
end;
then Y1
in M by
A1;
then F
c= Y1 by
SETFAM_1: 3;
then
[(
push (e,s)), y1]
in Y1 &
[(
push (e,s)), y1]
in
{
[(
push (e,s)), y1]} by
A23,
TARSKI:def 1;
hence contradiction by
XBOOLE_0:def 5;
end;
now
assume
A32: y2
<> d(e,y);
G[Y2]
proof
hereby
let s1 be
stack of X();
assume
A33:
emp s1;
then
A34:
[s1, e()]
in F by
A4;
not
emp (
push (e,s)) by
Def12;
then
[(
push (e,s)), y2]
<>
[s1, e()] by
A33,
XTUPLE_0: 1;
then
[s1, e()]
nin
{
[(
push (e,s)), y2]} by
TARSKI:def 1;
hence
[s1, e()]
in Y2 by
A34,
XBOOLE_0:def 5;
end;
let s1 be
stack of X(), a be
Element of X(), v be
Element of A();
assume
[s1, v]
in Y2;
then
A35:
[s1, v]
in F by
XBOOLE_0:def 5;
then
A36:
[(
push (a,s1)), d(a,v)]
in F by
A4;
now
assume
[(
push (e,s)), y2]
=
[(
push (a,s1)), d(a,v)];
then
A37: (
push (e,s))
= (
push (a,s1)) & y2
= d(a,v) by
XTUPLE_0: 1;
then e
= a & s
= s1 by
Th3;
hence contradiction by
A22,
A24,
A35,
A32,
A37;
end;
then
[(
push (a,s1)), d(a,v)]
nin
{
[(
push (e,s)), y2]} by
TARSKI:def 1;
hence
[(
push (a,s1)), d(a,v)]
in Y2 by
A36,
XBOOLE_0:def 5;
end;
then Y2
in M by
A1;
then F
c= Y2 by
SETFAM_1: 3;
then
[(
push (e,s)), y2]
in Y2 &
[(
push (e,s)), y2]
in
{
[(
push (e,s)), y2]} by
A23,
TARSKI:def 1;
hence contradiction by
XBOOLE_0:def 5;
end;
hence y1
= y2 by
A25;
end;
A38: F is
Function-like
proof
let x,y1,y2 be
object;
assume
A39:
[x, y1]
in F &
[x, y2]
in F;
then
reconsider x as
stack of X() by
ZFMISC_1: 87;
P[x] from
INDsch(
A11,
A21);
hence thesis by
A39;
end;
F is
quasi_total
proof
per cases ;
case A()
<>
{} ;
thus the
carrier' of X()
c= (
dom F)
proof
let x be
object;
assume x
in the
carrier' of X();
then
reconsider x as
stack of X();
Q[x] from
INDsch(
A6,
A8);
hence thesis by
XTUPLE_0:def 12;
end;
thus thesis;
end;
case A()
=
{} ;
hence thesis;
end;
end;
then
reconsider F as
Function of the
carrier' of X(), A() by
A38;
take a = (F
. s()), F;
thus a
= (F
. s());
hereby
let s1 be
stack of X();
assume
emp s1;
then
[s1, e()]
in F by
A4;
hence (F
. s1)
= e() by
FUNCT_1: 1;
end;
let s1 be
stack of X(), e be
Element of X();
(
dom F)
= the
carrier' of X() by
FUNCT_2:def 1;
then
[s1, (F
. s1)]
in F by
FUNCT_1:def 2;
then
[(
push (e,s1)), d(e,.)]
in F by
A4;
hence (F
. (
push (e,s1)))
= d(e,.) by
FUNCT_1: 1;
end;
scheme ::
STACKS_1:sch5
UNIQsch { X() ->
StackAlgebra , s() ->
stack of X() , A() -> non
empty
set , e() ->
Element of A() , d(
set,
set) ->
Element of A() } :
for a1,a2 be
Element of A() st (ex F be
Function of the
carrier' of X(), A() st a1
= (F
. s()) & (for s1 be
stack of X() st
emp s1 holds (F
. s1)
= e()) & for s1 be
stack of X(), e be
Element of X() holds (F
. (
push (e,s1)))
= d(e,.)) & (ex F be
Function of the
carrier' of X(), A() st a2
= (F
. s()) & (for s1 be
stack of X() st
emp s1 holds (F
. s1)
= e()) & for s1 be
stack of X(), e be
Element of X() holds (F
. (
push (e,s1)))
= d(e,.)) holds a1
= a2;
let a1,a2 be
Element of A();
given F1 be
Function of the
carrier' of X(), A() such that
A1: a1
= (F1
. s()) & (for s1 be
stack of X() st
emp s1 holds (F1
. s1)
= e()) & for s1 be
stack of X(), e be
Element of X() holds (F1
. (
push (e,s1)))
= d(e,.);
given F2 be
Function of the
carrier' of X(), A() such that
A2: a2
= (F2
. s()) & (for s1 be
stack of X() st
emp s1 holds (F2
. s1)
= e()) & for s1 be
stack of X(), e be
Element of X() holds (F2
. (
push (e,s1)))
= d(e,.);
defpred
P[
stack of X()] means (F1
. $1)
= (F2
. $1);
A3:
now
let s be
stack of X();
assume
emp s;
then (F1
. s)
= e() & (F2
. s)
= e() by
A1,
A2;
hence
P[s];
end;
A4:
now
let s be
stack of X(), e be
Element of X();
assume
P[s];
then (F1
. (
push (e,s)))
= d(e,.) by
A1;
hence
P[(
push (e,s))] by
A2;
end;
P[s()] from
INDsch(
A3,
A4);
hence a1
= a2 by
A1,
A2;
end;
begin
reserve X for
StackAlgebra;
reserve s,s1,s2,s3 for
stack of X;
reserve e,e1,e2,e3 for
Element of X;
definition
let X, s;
::
STACKS_1:def13
func
|.s.| ->
Element of (the
carrier of X
* ) means
:
Def13: ex F be
Function of the
carrier' of X, (the
carrier of X
* ) st it
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
=
{} ) & for s1, e holds (F
. (
push (e,s1)))
= (
<*e*>
^ (F
. s1));
existence
proof
deffunc
d(
Element of X,
Element of (the
carrier of X
* )) = (
<*$1*>
^ $2);
reconsider w = (
<*> the
carrier of X) as
Element of (the
carrier of X
* ) by
FINSEQ_1:def 11;
ex a be
Element of (the
carrier of X
* ) st ex F be
Function of the
carrier' of X, (the
carrier of X
* ) st a
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
= w) & for s1, e holds (F
. (
push (e,s1)))
=
d(e,) from
EXsch;
hence thesis;
end;
uniqueness
proof
deffunc
d(
Element of X,
Element of (the
carrier of X
* )) = (
<*$1*>
^ $2);
reconsider w = (
<*> the
carrier of X) as
Element of (the
carrier of X
* ) by
FINSEQ_1:def 11;
for a1,a2 be
Element of (the
carrier of X
* ) st (ex F be
Function of the
carrier' of X, (the
carrier of X
* ) st a1
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
= w) & for s1, e holds (F
. (
push (e,s1)))
=
d(e,)) & (ex F be
Function of the
carrier' of X, (the
carrier of X
* ) st a2
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
= w) & for s1, e holds (F
. (
push (e,s1)))
=
d(e,)) holds a1
= a2 from
UNIQsch;
hence thesis;
end;
end
theorem ::
STACKS_1:5
Th5:
emp s implies
|.s.|
=
{}
proof
ex F be
Function of the
carrier' of X, (the
carrier of X
* ) st
|.s.|
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
=
{} ) & for s1, e holds (F
. (
push (e,s1)))
= (
<*e*>
^ (F
. s1)) by
Def13;
hence thesis;
end;
theorem ::
STACKS_1:6
Th6: not
emp s implies
|.s.|
= (
<*(
top s)*>
^
|.(
pop s).|)
proof
consider F be
Function of the
carrier' of X, (the
carrier of X
* ) such that
A1:
|.s.|
= (F
. s) & (for s1 st
emp s1 holds (F
. s1)
=
{} ) & for s1, e holds (F
. (
push (e,s1)))
= (
<*e*>
^ (F
. s1)) by
Def13;
A2:
|.(
pop s).|
= (F
. (
pop s)) by
A1,
Def13;
assume not
emp s;
then s
= (
push ((
top s),(
pop s))) by
Def9;
hence thesis by
A1,
A2;
end;
theorem ::
STACKS_1:7
Th7: not
emp s implies
|.(
pop s).|
= (
Del (
|.s.|,1))
proof
assume not
emp s;
then
|.s.|
= (
<*(
top s)*>
^
|.(
pop s).|) by
Th6;
hence thesis by
WSIERP_1: 40;
end;
theorem ::
STACKS_1:8
Th8:
|.(
push (e,s)).|
= (
<*e*>
^
|.s.|)
proof
not
emp (
push (e,s)) by
Def12;
hence
|.(
push (e,s)).|
= (
<*(
top (
push (e,s)))*>
^
|.(
pop (
push (e,s))).|) by
Th6
.= (
<*e*>
^
|.(
pop (
push (e,s))).|) by
Def10
.= (
<*e*>
^
|.s.|) by
Def11;
end;
theorem ::
STACKS_1:9
Th9: not
emp s implies (
top s)
= (
|.s.|
. 1)
proof
assume not
emp s;
then
|.s.|
= (
<*(
top s)*>
^
|.(
pop s).|) by
Th6;
hence (
top s)
= (
|.s.|
. 1) by
FINSEQ_1: 41;
end;
theorem ::
STACKS_1:10
Th10:
|.s.|
=
{} implies
emp s
proof
assume
|.s.|
=
{} & not
emp s;
then
{}
= (
<*(
top s)*>
^
|.(
pop s).|) by
Th6;
hence thesis;
end;
theorem ::
STACKS_1:11
Th11: for s be
stack of (
StandardStackSystem A) holds
|.s.|
= s
proof
defpred
P[
stack of (
StandardStackSystem A)] means
|.$1.|
= $1;
A1:
now
let s be
stack of (
StandardStackSystem A);
assume
emp s;
then s
=
{} &
|.s.|
=
{} by
Def7,
Th5;
hence
P[s];
end;
A2:
now
let s be
stack of (
StandardStackSystem A);
let e be
Element of (
StandardStackSystem A);
assume
P[s];
then
|.(
push (e,s)).|
= (
<*e*>
^ s) by
Th8;
hence
P[(
push (e,s))] by
Def7;
end;
let s be
stack of (
StandardStackSystem A);
thus
P[s] from
INDsch(
A1,
A2);
end;
theorem ::
STACKS_1:12
Th12: for x be
Element of (the
carrier of X
* ) holds ex s st
|.s.|
= x
proof
set D = the
carrier of X;
defpred
P[
FinSequence of D] means ex s st
|.s.|
= $1;
A1:
P[(
<*> D)]
proof
consider s such that
A2:
emp s by
Th2;
take s;
thus thesis by
A2,
Th5;
end;
A3: for p be
FinSequence of D holds for x be
Element of D st
P[p] holds
P[(
<*x*>
^ p)]
proof
let p be
FinSequence of D, x be
Element of D;
given s such that
A4:
|.s.|
= p;
take s2 = (
push (x,s));
thus thesis by
A4,
Th8;
end;
for p be
FinSequence of D holds
P[p] from
IndSeqD(
A1,
A3);
hence thesis;
end;
definition
let X, s1, s2;
::
STACKS_1:def14
pred s1
== s2 means
|.s1.|
=
|.s2.|;
reflexivity ;
symmetry ;
end
theorem ::
STACKS_1:13
s1
== s2 & s2
== s3 implies s1
== s3;
theorem ::
STACKS_1:14
Th14: s1
== s2 &
emp s1 implies
emp s2
proof
assume
A1:
|.s1.|
=
|.s2.| &
emp s1;
assume not
emp s2;
then
|.s2.|
= (
<*(
top s2)*>
^
|.(
pop s2).|) by
Th6;
hence thesis by
A1,
Th5;
end;
theorem ::
STACKS_1:15
Th15:
emp s1 &
emp s2 implies s1
== s2
proof
assume
emp s1 &
emp s2;
then
|.s1.|
=
{} &
|.s2.|
=
{} by
Th5;
hence
|.s1.|
=
|.s2.|;
end;
theorem ::
STACKS_1:16
Th16: s1
== s2 implies (
push (e,s1))
== (
push (e,s2))
proof
assume
|.s1.|
=
|.s2.|;
hence
|.(
push (e,s1)).|
= (
<*e*>
^
|.s2.|) by
Th8
.=
|.(
push (e,s2)).| by
Th8;
end;
theorem ::
STACKS_1:17
Th17: s1
== s2 & not
emp s1 implies (
pop s1)
== (
pop s2)
proof
assume
A1: s1
== s2 & not
emp s1;
then
A2:
|.s1.|
=
|.s2.| & not
emp s2 by
Th14;
thus
|.(
pop s1).|
= (
Del (
|.s1.|,1)) by
A1,
Th7
.=
|.(
pop s2).| by
A2,
Th7;
end;
theorem ::
STACKS_1:18
Th18: s1
== s2 & not
emp s1 implies (
top s1)
= (
top s2)
proof
assume
A1: s1
== s2 & not
emp s1;
then
A2:
|.s1.|
=
|.s2.| & not
emp s2 by
Th14;
thus (
top s1)
= (
|.s1.|
. 1) by
A1,
Th9
.= (
top s2) by
A2,
Th9;
end;
definition
let X;
::
STACKS_1:def15
attr X is
proper-for-identity means
:
Def15: for s1, s2 st s1
== s2 holds s1
= s2;
end
registration
let A;
cluster (
StandardStackSystem A) ->
proper-for-identity;
coherence
proof
set X = (
StandardStackSystem A);
let s1,s2 be
stack of X;
assume
|.s1.|
=
|.s2.|;
hence s1
=
|.s2.| by
Th11
.= s2 by
Th11;
end;
end
definition
let X;
::
STACKS_1:def16
func
==_ X ->
Relation of the
carrier' of X means
:
Def16:
[s1, s2]
in it iff s1
== s2;
existence
proof
defpred
P[
stack of X,
stack of X] means $1
== $2;
thus ex R be
Relation of the
carrier' of X st for s1, s2 holds
[s1, s2]
in R iff
P[s1, s2] from
RELSET_1:sch 2;
end;
uniqueness
proof
defpred
P[
stack of X,
stack of X] means $1
== $2;
let R1,R2 be
Relation of the
carrier' of X such that
A1:
[s1, s2]
in R1 iff
P[s1, s2] and
A2:
[s1, s2]
in R2 iff
P[s1, s2];
thus thesis from
RELSET_1:sch 4(
A1,
A2);
end;
end
registration
let X;
cluster (
==_ X) ->
total
symmetric
transitive;
coherence
proof
set R = (
==_ X);
thus
A1: (
dom (
==_ X))
= the
carrier' of X
proof
thus (
dom R)
c= the
carrier' of X;
let x be
object;
assume x
in the
carrier' of X;
then
reconsider s = x as
stack of X;
[s, s]
in R by
Def16;
hence thesis by
XTUPLE_0:def 12;
end;
A2: (
field R)
= ((
dom R)
\/ (
rng R))
.= the
carrier' of X by
A1,
XBOOLE_1: 12;
thus (
==_ X) is
symmetric
proof
let x,y be
object;
assume x
in (
field R) & y
in (
field R);
then
reconsider s1 = x, s2 = y as
stack of X by
A2;
assume
[x, y]
in R;
then s1
== s2 by
Def16;
hence thesis by
Def16;
end;
let x,y,z be
object;
assume x
in (
field R) & y
in (
field R) & z
in (
field R);
then
reconsider s1 = x, s2 = y, s3 = z as
stack of X by
A2;
assume
[x, y]
in R &
[y, z]
in R;
then s1
== s2 & s2
== s3 by
Def16;
then s1
== s3;
hence thesis by
Def16;
end;
end
theorem ::
STACKS_1:19
Th19:
emp s implies (
Class ((
==_ X),s))
= the
s_empty of X
proof
assume
A1:
emp s;
thus (
Class ((
==_ X),s))
c= the
s_empty of X
proof
let x be
object;
assume
A2: x
in (
Class ((
==_ X),s));
then
reconsider s1 = x as
stack of X;
[s, s1]
in (
==_ X) by
A2,
EQREL_1: 18;
then s
== s1 by
Def16;
then
emp s1 by
A1,
Th14;
hence thesis;
end;
let x be
object;
assume
A3: x
in the
s_empty of X;
then
reconsider s1 = x as
stack of X;
emp s1 by
A3;
then s
== s1 by
A1,
Th15;
then
[s, s1]
in (
==_ X) by
Def16;
hence thesis by
EQREL_1: 18;
end;
definition
let X, s;
::
STACKS_1:def17
func
coset s ->
Subset of the
carrier' of X means
:
Def17: s
in it & (for e, s1 st s1
in it holds (
push (e,s1))
in it & ( not
emp s1 implies (
pop s1)
in it )) & for A be
Subset of the
carrier' of X st s
in A & (for e, s1 st s1
in A holds (
push (e,s1))
in A & ( not
emp s1 implies (
pop s1)
in A)) holds it
c= A;
existence
proof
defpred
P[
set] means s
in $1 & (for e, s1 st s1
in $1 holds (
push (e,s1))
in $1 & ( not
emp s1 implies (
pop s1)
in $1));
consider Y be
set such that
A1: x
in Y iff x
in (
bool the
carrier' of X) &
P[x] from
XFAMILY:sch 1;
set S = the
carrier' of X;
A2:
P[the
carrier' of X] & S
in (
bool S) by
ZFMISC_1:def 1;
then
A3: the
carrier' of X
in Y by
A1;
reconsider Y as non
empty
set by
A2,
A1;
reconsider C = (
meet Y) as
Subset of S by
A3,
SETFAM_1: 3;
take C;
for x st x
in Y holds s
in x by
A1;
hence s
in C by
SETFAM_1:def 1;
hereby
let e, s1;
assume
A4: s1
in C;
now
let x;
assume
A5: x
in Y;
then s1
in x by
A4,
SETFAM_1:def 1;
hence (
push (e,s1))
in x by
A1,
A5;
end;
hence (
push (e,s1))
in C by
SETFAM_1:def 1;
assume
A6: not
emp s1;
now
let x;
assume
A7: x
in Y;
then s1
in x by
A4,
SETFAM_1:def 1;
hence (
pop s1)
in x by
A1,
A6,
A7;
end;
hence (
pop s1)
in C by
SETFAM_1:def 1;
end;
let A be
Subset of the
carrier' of X;
assume
P[A];
then A
in Y by
A1;
hence C
c= A by
SETFAM_1: 3;
end;
uniqueness ;
end
theorem ::
STACKS_1:20
Th20: ((
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
(
pop (
push (e,s)))
= s & not
emp (
push (e,s)) by
Def11,
Def12;
hence (
push (e,s))
in (
coset s1) implies s
in (
coset s1) by
Def17;
assume not
emp s;
then (
push ((
top s),(
pop s)))
= s by
Def9;
hence thesis by
Def17;
end;
theorem ::
STACKS_1:21
s
in (
coset (
push (e,s))) & ( not
emp s implies s
in (
coset (
pop s)))
proof
(
pop (
push (e,s)))
= s & not
emp (
push (e,s)) & (
push (e,s))
in (
coset (
push (e,s))) by
Def11,
Def12,
Def17;
hence s
in (
coset (
push (e,s))) by
Def17;
assume not
emp s;
then (
push ((
top s),(
pop s)))
= s & (
pop s)
in (
coset (
pop s)) by
Def9,
Def17;
hence thesis by
Def17;
end;
theorem ::
STACKS_1:22
ex s1 st
emp s1 & s1
in (
coset s)
proof
deffunc
F(
stack of X) = (
pop $1);
defpred
P[
set,
stack of X,
set] means $3
= (
IFIN ($2,the
s_empty of X,s,(
pop $2)));
A1: for n be
Nat holds for x be
stack of X holds ex y be
stack of X st
P[n, x, y];
consider f be
sequence of the
carrier' of X such that
A2: (f
.
0 )
= s & for i be
Nat holds
P[i, (f
. i), (f
. (i
+ 1))] from
RECDEF_1:sch 2(
A1);
defpred
Q[
Nat] means (f
. $1)
in (
coset s);
A3:
Q[
0 ] by
A2,
Def17;
A4:
now
let i;
assume
A5:
Q[i];
(f
. (i
+ 1))
= (
IFIN ((f
. i),the
s_empty of X,s,(
pop (f
. i)))) by
A2;
then ((f
. i)
in the
s_empty of X implies (f
. (i
+ 1))
= s) & ((f
. i)
nin the
s_empty of X implies (f
. (i
+ 1))
= (
pop (f
. i))) by
MATRIX_7:def 1;
then (f
. (i
+ 1))
= s or not
emp (f
. i) & (f
. (i
+ 1))
= (
pop (f
. i));
hence
Q[(i
+ 1)] by
A5,
Def17;
end;
A6:
Q[i] from
NAT_1:sch 2(
A3,
A4);
consider i, s1 such that
A7: (f
. i)
= s1 & ( not
emp s1 implies (f
. (i
+ 1))
<> (
pop s1)) by
Def8;
take s1;
(f
. (i
+ 1))
= (
IFIN ((f
. i),the
s_empty of X,s,(
pop (f
. i)))) by
A2;
then ((f
. i)
in the
s_empty of X implies (f
. (i
+ 1))
= s) & ((f
. i)
nin the
s_empty of X implies (f
. (i
+ 1))
= (
pop (f
. i))) by
MATRIX_7:def 1;
hence thesis by
A7,
A6;
end;
registration
let A;
let R be
Relation of A;
cluster A
-valued for
RedSequence of R;
existence
proof
set a = the
Element of A;
reconsider t =
<*a*> as
RedSequence of R by
REWRITE1: 6;
take t;
thus thesis;
end;
end
definition
let X;
::
STACKS_1:def18
func
ConstructionRed X ->
Relation of the
carrier' of X means
:
Def18:
[s1, s2]
in it iff ( not
emp s1 & s2
= (
pop s1)) or ex e st s2
= (
push (e,s1));
existence
proof
defpred
P[
stack of X,
stack of X] means ( not
emp $1 & $2
= (
pop $1)) or ex e st $2
= (
push (e,$1));
thus ex R be
Relation of the
carrier' of X st for s1, s2 holds
[s1, s2]
in R iff
P[s1, s2] from
RELSET_1:sch 2;
end;
uniqueness
proof
defpred
P[
stack of X,
stack of X] means ( not
emp $1 & $2
= (
pop $1)) or ex e st $2
= (
push (e,$1));
let R1,R2 be
Relation of the
carrier' of X such that
A1:
[s1, s2]
in R1 iff
P[s1, s2] and
A2:
[s1, s2]
in R2 iff
P[s1, s2];
thus thesis from
RELSET_1:sch 4(
A1,
A2);
end;
end
theorem ::
STACKS_1:23
Th23: for R be
Relation of A holds for t be
RedSequence of R holds (t
. 1)
in A iff t is A
-valued
proof
let R be
Relation of A;
let t be
RedSequence of R;
(
rng t)
<>
{} ;
then 1
in (
dom t) by
FINSEQ_3: 32;
then
A1: (t
. 1)
in (
rng t) by
FUNCT_1:def 3;
hereby
assume
A2: (t
. 1)
in A;
defpred
P[
Nat] means $1
in (
dom t) implies (t
. $1)
in A;
A3:
P[
0 ] by
FINSEQ_3: 24;
A4:
P[i] implies
P[(i
+ 1)]
proof
assume
P[i];
assume
A5: (i
+ 1)
in (
dom t) & (t
. (i
+ 1))
nin A;
i
=
0 or i
>= (
0
+ 1) by
NAT_1: 13;
then
consider j be
Nat such that
A6: i
= (j
+ 1) by
A2,
A5,
NAT_1: 6;
i
<= (i
+ 1) & (i
+ 1)
<= (
len t) by
A5,
FINSEQ_3: 25,
NAT_1: 11;
then 1
<= i & i
<= (
len t) by
A6,
NAT_1: 11,
XXREAL_0: 2;
then i
in (
dom t) by
FINSEQ_3: 25;
then
[(t
. i), (t
. (i
+ 1))]
in R by
A5,
REWRITE1:def 2;
hence thesis by
A5,
ZFMISC_1: 87;
end;
A7:
P[i] from
NAT_1:sch 2(
A3,
A4);
thus t is A
-valued
proof
let x be
object;
assume x
in (
rng t);
then
consider y be
object such that
A8: y
in (
dom t) & x
= (t
. y) by
FUNCT_1:def 3;
reconsider y as
Nat by
A8;
thus thesis by
A8,
A7;
end;
end;
assume (
rng t)
c= A;
hence (t
. 1)
in A by
A1;
end;
scheme ::
STACKS_1:sch6
PathIND { X() -> non
empty
set , x1,x2() ->
Element of X() , R() ->
Relation of X() , P[
set] } :
P[x2()]
provided
A1: P[x1()]
and
A2: R()
reduces (x1(),x2())
and
A3: for x,y be
Element of X() st R()
reduces (x1(),x) &
[x, y]
in R() & P[x] holds P[y];
consider t be
RedSequence of R() such that
A4: (t
. 1)
= x1() & (t
. (
len t))
= x2() by
A2;
reconsider t as X()
-valued
RedSequence of R() by
A4,
Th23;
defpred
Q[
Nat] means $1
in (
dom t) implies P[(t
. $1)];
A5:
Q[
0 ] by
FINSEQ_3: 24;
A6:
now
let i;
assume
A7:
Q[i];
thus
Q[(i
+ 1)]
proof
assume
A8: (i
+ 1)
in (
dom t) & not P[(t
. (i
+ 1))];
i
=
0 or i
>= (
0
+ 1) by
NAT_1: 13;
then
consider j be
Nat such that
A9: i
= (j
+ 1) by
A1,
A4,
A8,
NAT_1: 6;
i
<= (i
+ 1) & (i
+ 1)
<= (
len t) by
A8,
FINSEQ_3: 25,
NAT_1: 11;
then
A10: 1
<= i & i
<= (
len t) & (
rng t)
<>
{} by
A9,
NAT_1: 11,
XXREAL_0: 2;
then
A11: i
in (
dom t) & 1
in (
dom t) by
FINSEQ_3: 25,
FINSEQ_3: 32;
A12: (t
. i)
= (t
/. i) & (t
. (i
+ 1))
= (t
/. (i
+ 1)) by
A8,
A11,
PARTFUN1:def 6;
then
[(t
/. i), (t
/. (i
+ 1))]
in R() by
A8,
A11,
REWRITE1:def 2;
hence thesis by
A3,
A7,
A8,
A11,
A4,
A10,
A12,
REWRITE1: 17;
end;
end;
A13:
Q[i] from
NAT_1:sch 2(
A5,
A6);
(
len t)
in (
dom t) by
FINSEQ_5: 6;
hence thesis by
A4,
A13;
end;
theorem ::
STACKS_1:24
Th24: for t be
RedSequence of (
ConstructionRed X) st s
= (t
. 1) holds (
rng t)
c= (
coset s)
proof
set R = (
ConstructionRed X);
let t be
RedSequence of (
ConstructionRed X);
assume
A1: s
= (t
. 1);
then
reconsider u = t as the
carrier' of X
-valued
RedSequence of R by
Th23;
defpred
Q[
Nat] means $1
in (
dom t) implies (t
. $1)
in (
coset s);
A2:
Q[
0 ] by
FINSEQ_3: 24;
A3:
now
let i;
assume
A4:
Q[i];
thus
Q[(i
+ 1)]
proof
assume
A5: (i
+ 1)
in (
dom t) & (t
. (i
+ 1))
nin (
coset s);
i
=
0 or i
>= (
0
+ 1) by
NAT_1: 13;
then
consider j be
Nat such that
A6: i
= (j
+ 1) by
A1,
A5,
Def17,
NAT_1: 6;
i
<= (i
+ 1) & (i
+ 1)
<= (
len t) by
A5,
FINSEQ_3: 25,
NAT_1: 11;
then
A7: 1
<= i & i
<= (
len t) & (
rng t)
<>
{} by
A6,
NAT_1: 11,
XXREAL_0: 2;
then
A8: i
in (
dom t) & 1
in (
dom t) by
FINSEQ_3: 25,
FINSEQ_3: 32;
then
A9: (t
. i)
= (u
/. i) & (t
. (i
+ 1))
= (u
/. (i
+ 1)) by
A5,
PARTFUN1:def 6;
then
[(u
/. i), (u
/. (i
+ 1))]
in R by
A5,
A8,
REWRITE1:def 2;
then ( not
emp (u
/. i) & (u
/. (i
+ 1))
= (
pop (u
/. i))) or ex e st (u
/. (i
+ 1))
= (
push (e,(u
/. i))) by
Def18;
hence thesis by
A4,
A5,
A7,
A9,
Def17,
FINSEQ_3: 25;
end;
end;
A10:
Q[i] from
NAT_1:sch 2(
A2,
A3);
let x be
object;
assume x
in (
rng t);
then ex y be
object st y
in (
dom t) & x
= (t
. y) by
FUNCT_1:def 3;
hence thesis by
A10;
end;
theorem ::
STACKS_1:25
Th25: (
coset s)
= { s1 : (
ConstructionRed X)
reduces (s,s1) }
proof
set R = (
ConstructionRed X);
A1: { s1 : R
reduces (s,s1) }
c= the
carrier' of X
proof
let x be
object;
assume x
in { s1 : R
reduces (s,s1) };
then ex s1 st x
= s1 & R
reduces (s,s1);
hence thesis;
end;
R
reduces (s,s) by
REWRITE1: 12;
then
A2: s
in { s1 : R
reduces (s,s1) };
now
let e, s2;
assume s2
in { s1 : R
reduces (s,s1) };
then
A3: ex s1 st s2
= s1 & R
reduces (s,s1);
[s2, (
push (e,s2))]
in R by
Def18;
then R
reduces (s2,(
push (e,s2))) by
REWRITE1: 15;
then R
reduces (s,(
push (e,s2))) by
A3,
REWRITE1: 16;
hence (
push (e,s2))
in { s1 : R
reduces (s,s1) };
assume not
emp s2;
then
[s2, (
pop s2)]
in R by
Def18;
then R
reduces (s2,(
pop s2)) by
REWRITE1: 15;
then R
reduces (s,(
pop s2)) by
A3,
REWRITE1: 16;
hence (
pop s2)
in { s1 : R
reduces (s,s1) };
end;
hence (
coset s)
c= { s1 : R
reduces (s,s1) } by
A1,
A2,
Def17;
let x be
object;
assume x
in { s1 : R
reduces (s,s1) };
then
consider s1 such that
A4: x
= s1 & R
reduces (s,s1);
consider t be
RedSequence of R such that
A5: s
= (t
. 1) & s1
= (t
. (
len t)) by
A4;
(
len t)
in (
dom t) by
FINSEQ_5: 6;
then x
in (
rng t) & (
rng t)
c= (
coset s) by
A4,
A5,
Th24,
FUNCT_1:def 3;
hence thesis;
end;
definition
let X, s;
::
STACKS_1:def19
func
core s ->
stack of X means
:
Def19:
emp it & ex t be the
carrier' of X
-valued
RedSequence of (
ConstructionRed X) st (t
. 1)
= s & (t
. (
len t))
= it & for i st 1
<= i & i
< (
len t) holds not
emp (t
/. i) & (t
/. (i
+ 1))
= (
pop (t
/. i));
existence
proof
set R = (
ConstructionRed X);
deffunc
F(
stack of X) = (
pop $1);
defpred
P[
set,
stack of X,
set] means $3
= (
IFIN ($2,the
s_empty of X,s,(
pop $2)));
A1: for n be
Nat holds for x be
stack of X holds ex y be
stack of X st
P[n, x, y];
consider f be
sequence of the
carrier' of X such that
A2: (f
.
0 )
= s & for i be
Nat holds
P[i, (f
. i), (f
. (i
+ 1))] from
RECDEF_1:sch 2(
A1);
defpred
R[
Nat] means ex s1 st (f
. $1)
= s1 & ( not
emp s1 implies (f
. ($1
+ 1))
<> (
pop s1));
A3: ex i st
R[i] by
Def8;
consider i such that
A4:
R[i] & for j be
Nat st
R[j] holds i
<= j from
NAT_1:sch 5(
A3);
deffunc
F(
Nat) = (f
. ($1
-' 1));
consider t be
FinSequence such that
A5: (
len t)
= (i
+ 1) & for j be
Nat st j
in (
dom t) holds (t
. j)
=
F(j) from
FINSEQ_1:sch 2;
consider s1 such that
A6: (f
. i)
= s1 & ( not
emp s1 implies (f
. (i
+ 1))
<> (
pop s1)) by
A4;
take s1;
(f
. (i
+ 1))
= (
IFIN ((f
. i),the
s_empty of X,s,(
pop (f
. i)))) by
A2;
then ((f
. i)
in the
s_empty of X implies (f
. (i
+ 1))
= s) & ((f
. i)
nin the
s_empty of X implies (f
. (i
+ 1))
= (
pop (f
. i))) by
MATRIX_7:def 1;
hence
emp s1 by
A6;
A7: t is
RedSequence of R
proof
thus (
len t)
>
0 by
A5;
let j be
Nat;
assume
A8: j
in (
dom t) & (j
+ 1)
in (
dom t);
then j
>= 1 & j
<= (i
+ 1) & (j
+ 1)
<= (i
+ 1) by
A5,
FINSEQ_3: 25;
then
A9: ((j
-' 1)
+ 1)
= j & ((j
+ 1)
-' 1)
= j & j
<= i by
NAT_D: 34,
XREAL_1: 6,
XREAL_1: 235;
(j
-' 1)
< i by
A9,
NAT_1: 13;
then
A10: not
emp (f
. (j
-' 1)) by
A4;
then
A11: (f
. (j
-' 1))
nin the
s_empty of X;
A12: (t
. j)
= (f
. (j
-' 1)) & (t
. (j
+ 1))
= (f
. j) by
A5,
A8,
A9;
then
P[(j
-' 1), (f
. (j
-' 1)), (t
. (j
+ 1))] by
A2,
A9;
then (t
. (j
+ 1))
= (
pop (f
. (j
-' 1))) by
A11,
MATRIX_7:def 1;
hence
[(t
. j), (t
. (j
+ 1))]
in R by
A12,
A10,
Def18;
end;
then 1
in (
dom t) by
FINSEQ_5: 6;
then
A13: (t
. 1)
= (f
. (1
-' 1)) by
A5
.= s by
A2,
XREAL_1: 232;
then
reconsider t as the
carrier' of X
-valued
RedSequence of R by
A7,
Th23;
take t;
thus (t
. 1)
= s by
A13;
(
len t)
in (
dom t) by
FINSEQ_5: 6;
hence (t
. (
len t))
= (f
. ((i
+ 1)
-' 1)) by
A5
.= s1 by
A6,
NAT_D: 34;
let k be
Nat;
assume
A14: 1
<= k & k
< (
len t);
then k
in (
dom t) by
FINSEQ_3: 25;
then
A15: (t
. k)
= (f
. (k
-' 1)) & (t
. k)
= (t
/. k) by
A5,
PARTFUN1:def 6;
1
<= (k
+ 1) & (k
+ 1)
<= (
len t) by
A14,
NAT_1: 13;
then (k
+ 1)
in (
dom t) by
FINSEQ_3: 25;
then
A16: (t
. (k
+ 1))
= (f
. ((k
+ 1)
-' 1)) & (t
. (k
+ 1))
= (t
/. (k
+ 1)) by
A5,
PARTFUN1:def 6;
A17: ((k
-' 1)
+ 1)
= k & ((k
+ 1)
-' 1)
= k by
A14,
NAT_D: 34,
XREAL_1: 235;
then (k
-' 1)
< i by
A5,
A14,
XREAL_1: 6;
hence not
emp (t
/. k) by
A4,
A15;
then
A18: (t
/. k)
nin the
s_empty of X;
(f
. k)
= (
IFIN ((f
. (k
-' 1)),the
s_empty of X,s,(
pop (f
. (k
-' 1))))) by
A2,
A17;
hence (t
/. (k
+ 1))
= (
pop (t
/. k)) by
A15,
A16,
A17,
A18,
MATRIX_7:def 1;
end;
uniqueness
proof
let x1,x2 be
stack of X such that
A19:
emp x1;
given t1 be the
carrier' of X
-valued
RedSequence of (
ConstructionRed X) such that
A20: (t1
. 1)
= s & (t1
. (
len t1))
= x1 and
A21: for i st 1
<= i & i
< (
len t1) holds not
emp (t1
/. i) & (t1
/. (i
+ 1))
= (
pop (t1
/. i));
assume
A22:
emp x2;
given t2 be the
carrier' of X
-valued
RedSequence of (
ConstructionRed X) such that
A23: (t2
. 1)
= s & (t2
. (
len t2))
= x2 and
A24: for i st 1
<= i & i
< (
len t2) holds not
emp (t2
/. i) & (t2
/. (i
+ 1))
= (
pop (t2
/. i));
A25: (
len t1)
in (
dom t1) & (
len t2)
in (
dom t2) & 1
in (
dom t1) & 1
in (
dom t2) by
FINSEQ_5: 6;
defpred
P[
Nat] means ($1
in (
dom t1) iff $1
in (
dom t2)) & ($1
in (
dom t1) implies (t1
. $1)
= (t2
. $1));
A26:
P[
0 ] by
FINSEQ_3: 24;
A27:
P[i] implies
P[(i
+ 1)]
proof
assume
A28:
P[i];
per cases by
NAT_1: 6;
suppose i
=
0 ;
hence thesis by
A20,
A23,
FINSEQ_5: 6;
end;
suppose ex j st i
= (j
+ 1);
then
consider j such that
A29: i
= (j
+ 1);
A30: i
>= 1 by
A29,
NAT_1: 11;
now
assume (i
+ 1)
in (
dom t1);
then (i
+ 1)
<= (
len t1) by
FINSEQ_3: 25;
then i
< (
len t1) by
NAT_1: 13;
then i
in (
dom t1) & not
emp (t1
/. i) by
A21,
A30,
FINSEQ_3: 25;
then (
len t2)
<> i & i
<= (
len t2) by
A22,
A23,
A28,
FINSEQ_3: 25,
PARTFUN1:def 6;
then i
< (
len t2) by
XXREAL_0: 1;
then 1
<= (i
+ 1) & (i
+ 1)
<= (
len t2) by
NAT_1: 11,
NAT_1: 13;
hence (i
+ 1)
in (
dom t2) by
FINSEQ_3: 25;
end;
hereby
assume (i
+ 1)
in (
dom t2);
then (i
+ 1)
<= (
len t2) by
FINSEQ_3: 25;
then i
< (
len t2) by
NAT_1: 13;
then i
in (
dom t2) & not
emp (t2
/. i) by
A24,
A30,
FINSEQ_3: 25;
then (
len t1)
<> i & i
<= (
len t1) by
A19,
A20,
A28,
FINSEQ_3: 25,
PARTFUN1:def 6;
then i
< (
len t1) by
XXREAL_0: 1;
then 1
<= (i
+ 1) & (i
+ 1)
<= (
len t1) by
NAT_1: 11,
NAT_1: 13;
hence (i
+ 1)
in (
dom t1) by
FINSEQ_3: 25;
end;
assume
A32: (i
+ 1)
in (
dom t1);
then (i
+ 1)
<= (
len t1) & (i
+ 1)
<= (
len t2) by
A31,
FINSEQ_3: 25;
then i
< (
len t1) & i
< (
len t2) by
NAT_1: 13;
then
A33: i
in (
dom t1) & (t1
/. (i
+ 1))
= (
pop (t1
/. i)) & i
in (
dom t2) & (t2
/. (i
+ 1))
= (
pop (t2
/. i)) by
A21,
A24,
A30,
FINSEQ_3: 25;
then (t1
/. i)
= (t1
. i) & (t2
/. i)
= (t2
. i) & (t1
/. (i
+ 1))
= (t1
. (i
+ 1)) & (t2
/. (i
+ 1))
= (t2
. (i
+ 1)) by
A32,
A31,
PARTFUN1:def 6;
hence thesis by
A28,
A33;
end;
end;
A34:
P[i] from
NAT_1:sch 2(
A26,
A27);
(
dom t1)
= (
dom t2)
proof
thus (
dom t1)
c= (
dom t2) by
A34;
let x be
object;
thus thesis by
A34;
end;
then (
len t1)
= (
len t2) by
FINSEQ_3: 29;
hence thesis by
A20,
A23,
A25,
A34;
end;
end
theorem ::
STACKS_1:26
Th26:
emp s implies (
core s)
= s
proof
set R = (
ConstructionRed X);
assume
A1:
emp s;
consider t be the
carrier' of X
-valued
RedSequence of R such that
A2: (t
. 1)
= s & (t
. (
len t))
= (
core s) and
A3: for i st 1
<= i & i
< (
len t) holds not
emp (t
/. i) & (t
/. (i
+ 1))
= (
pop (t
/. i)) by
Def19;
A4: 1
in (
dom t) by
FINSEQ_5: 6;
then (t
/. 1)
= (t
. 1) by
PARTFUN1:def 6;
then 1
<= (
len t) & (
len t)
<= 1 by
A1,
A2,
A3,
A4,
FINSEQ_3: 25;
hence thesis by
A2,
XXREAL_0: 1;
end;
theorem ::
STACKS_1:27
Th27: (
core (
push (e,s)))
= (
core s)
proof
set R = (
ConstructionRed X);
set A = the
carrier' of X;
A1:
emp (
core s) by
Def19;
consider t be the
carrier' of X
-valued
RedSequence of R such that
A2: (t
. 1)
= s & (t
. (
len t))
= (
core s) and
A3: for i st 1
<= i & i
< (
len t) holds not
emp (t
/. i) & (t
/. (i
+ 1))
= (
pop (t
/. i)) by
Def19;
not
emp (
push (e,s)) & (
pop (
push (e,s)))
= s by
Def11,
Def12;
then
[(
push (e,s)), s]
in R by
Def18;
then
reconsider u =
<*(
push (e,s)), s*> as
RedSequence of R by
REWRITE1: 7;
(u
. 2)
= s & (
len u)
= 2 by
FINSEQ_1: 44;
then
reconsider v = (u
$^ t) as
RedSequence of R by
A2,
REWRITE1: 8;
A4: v
= (
<*(
push (e,s))*>
^ t) by
REWRITE1: 2;
then
A5: (v
. 1)
= (
push (e,s)) by
FINSEQ_1: 41;
then
reconsider v as A
-valued
RedSequence of R by
Th23;
A6: (
len
<*(
push (e,s))*>)
= 1 by
FINSEQ_1: 40;
then
A7: (
len v)
= (1
+ (
len t)) by
A4,
FINSEQ_1: 22;
(
len t)
in (
dom t) by
FINSEQ_5: 6;
then
A8: (v
. (
len v))
= (t
. (
len t)) by
A4,
A6,
A7,
FINSEQ_1:def 7;
now
let i;
assume
A9: 1
<= i & i
< (
len v);
i
in (
dom v) & (i
+ 1)
in (
dom v) by
A9,
MSUALG_8: 1;
then
A10: (v
/. i)
= (v
. i) & (v
/. (i
+ 1))
= (v
. (i
+ 1)) by
PARTFUN1:def 6;
consider j such that
A11: i
= (1
+ j) by
A9,
NAT_1: 10;
A12: j
< (
len t) by
A7,
A9,
A11,
XREAL_1: 6;
per cases by
A9,
XXREAL_0: 1;
suppose
A13: i
= 1;
hence not
emp (v
/. i) by
A5,
A10,
Def12;
1
in (
dom t) by
FINSEQ_5: 6;
hence (v
/. (i
+ 1))
= (t
. 1) by
A4,
A6,
A10,
A13,
FINSEQ_1:def 7
.= (
pop (v
/. i)) by
A13,
A2,
A5,
A10,
Def11;
end;
suppose i
> 1;
then
A14: j
>= 1 & j
in
NAT by
A11,
NAT_1: 13,
ORDINAL1:def 12;
then j
in (
dom t) & i
in (
dom t) by
A11,
A12,
MSUALG_8: 1;
then (t
. j)
= (v
. i) & (t
/. j)
= (t
. j) & (t
. i)
= (v
. (i
+ 1)) & (t
/. i)
= (t
. i) by
A4,
A6,
A11,
FINSEQ_1:def 7,
PARTFUN1:def 6;
hence not
emp (v
/. i) & (v
/. (i
+ 1))
= (
pop (v
/. i)) by
A3,
A10,
A11,
A12,
A14;
end;
end;
hence thesis by
A1,
A2,
A5,
A8,
Def19;
end;
theorem ::
STACKS_1:28
Th28: not
emp s implies (
core (
pop s))
= (
core s)
proof
set R = (
ConstructionRed X);
set A = the
carrier' of X;
assume
A1: not
emp s;
A2:
emp (
core (
pop s)) by
Def19;
consider t be the
carrier' of X
-valued
RedSequence of R such that
A3: (t
. 1)
= (
pop s) & (t
. (
len t))
= (
core (
pop s)) and
A4: for i st 1
<= i & i
< (
len t) holds not
emp (t
/. i) & (t
/. (i
+ 1))
= (
pop (t
/. i)) by
Def19;
[s, (
pop s)]
in R by
A1,
Def18;
then
reconsider u =
<*s, (
pop s)*> as
RedSequence of R by
REWRITE1: 7;
(u
. 2)
= (
pop s) & (
len u)
= 2 by
FINSEQ_1: 44;
then
reconsider v = (u
$^ t) as
RedSequence of R by
A3,
REWRITE1: 8;
A5: v
= (
<*s*>
^ t) by
REWRITE1: 2;
then
A6: (v
. 1)
= s by
FINSEQ_1: 41;
then
reconsider v as A
-valued
RedSequence of R by
Th23;
A7: (
len
<*s*>)
= 1 by
FINSEQ_1: 40;
then
A8: (
len v)
= (1
+ (
len t)) by
A5,
FINSEQ_1: 22;
(
len t)
in (
dom t) by
FINSEQ_5: 6;
then
A9: (v
. (
len v))
= (t
. (
len t)) by
A5,
A7,
A8,
FINSEQ_1:def 7;
now
let i;
assume
A10: 1
<= i & i
< (
len v);
i
in (
dom v) & (i
+ 1)
in (
dom v) by
A10,
MSUALG_8: 1;
then
A11: (v
/. i)
= (v
. i) & (v
/. (i
+ 1))
= (v
. (i
+ 1)) by
PARTFUN1:def 6;
consider j such that
A12: i
= (1
+ j) by
A10,
NAT_1: 10;
A13: j
< (
len t) by
A8,
A10,
A12,
XREAL_1: 6;
per cases by
A10,
XXREAL_0: 1;
suppose
A14: i
= 1;
hence not
emp (v
/. i) by
A1,
A5,
A11,
FINSEQ_1: 41;
1
in (
dom t) by
FINSEQ_5: 6;
hence (v
/. (i
+ 1))
= (t
. 1) by
A5,
A7,
A11,
A14,
FINSEQ_1:def 7
.= (
pop (v
/. i)) by
A14,
A3,
A5,
A11,
FINSEQ_1: 41;
end;
suppose i
> 1;
then
A15: j
>= 1 & j
in
NAT by
A12,
NAT_1: 13,
ORDINAL1:def 12;
then j
in (
dom t) & i
in (
dom t) by
A12,
A13,
MSUALG_8: 1;
then (t
. j)
= (v
. i) & (t
/. j)
= (t
. j) & (t
. i)
= (v
. (i
+ 1)) & (t
/. i)
= (t
. i) by
A5,
A7,
A12,
FINSEQ_1:def 7,
PARTFUN1:def 6;
hence not
emp (v
/. i) & (v
/. (i
+ 1))
= (
pop (v
/. i)) by
A4,
A11,
A12,
A13,
A15;
end;
end;
hence thesis by
A2,
A3,
A6,
A9,
Def19;
end;
theorem ::
STACKS_1:29
Th29: (
core s)
in (
coset s)
proof
consider t be the
carrier' of X
-valued
RedSequence of (
ConstructionRed X) such that
A1: (t
. 1)
= s & (t
. (
len t))
= (
core s) and for i st 1
<= i & i
< (
len t) holds not
emp (t
/. i) & (t
/. (i
+ 1))
= (
pop (t
/. i)) by
Def19;
(
ConstructionRed X)
reduces (s,(
core s)) by
A1;
then (
core s)
in { s1 : (
ConstructionRed X)
reduces (s,s1) };
hence thesis by
Th25;
end;
theorem ::
STACKS_1:30
Th30: for x be
Element of (the
carrier of X
* ) holds ex s1 st
|.s1.|
= x & s1
in (
coset s)
proof
set A = the
carrier of X;
defpred
P[
FinSequence of A] means ex s1 st
|.s1.|
= $1 & s1
in (
coset s);
emp (
core s) by
Def19;
then
|.(
core s).|
=
{} by
Th5;
then
A1:
P[(
<*> A)] by
Th29;
A2:
now
let p be
FinSequence of A;
let x be
Element of A;
assume
P[p];
then
consider s1 such that
A3:
|.s1.|
= p & s1
in (
coset s);
thus
P[(
<*x*>
^ p)]
proof
take s2 = (
push (x,s1));
thus thesis by
A3,
Th8,
Def17;
end;
end;
for p be
FinSequence of A holds
P[p] from
IndSeqD(
A1,
A2);
hence thesis;
end;
theorem ::
STACKS_1:31
Th31: s1
in (
coset s) implies (
core s1)
= (
core s)
proof
assume
A1: s1
in (
coset s);
set R = (
ConstructionRed X);
defpred
P[
stack of X] means (
core $1)
= (
core s);
A2:
P[s];
(
coset s)
= { s2 : R
reduces (s,s2) } by
Th25;
then ex s2 st s1
= s2 & R
reduces (s,s2) by
A1;
then
A3: R
reduces (s,s1);
A4:
now
let x,y be
stack of X;
assume
A5: R
reduces (s,x) &
[x, y]
in R &
P[x];
then not
emp x & y
= (
pop x) or ex e st y
= (
push (e,x)) by
Def18;
hence
P[y] by
A5,
Th27,
Th28;
end;
thus
P[s1] from
PathIND(
A2,
A3,
A4);
end;
theorem ::
STACKS_1:32
Th32: s1
in (
coset s) & s2
in (
coset s) &
|.s1.|
=
|.s2.| implies s1
= s2
proof
defpred
P[
stack of X] means for s2 st $1
in (
coset s) & s2
in (
coset s) &
|.$1.|
=
|.s2.| holds $1
= s2;
A1: for s1 st
emp s1 holds
P[s1]
proof
let s1;
assume
A2:
emp s1;
then
A3:
|.s1.|
=
{} by
Th5;
let s2;
assume s1
in (
coset s) & s2
in (
coset s) &
|.s1.|
=
|.s2.|;
then (
core s1)
= (
core s) & (
core s2)
= (
core s) &
emp s2 by
A3,
Th10,
Th31;
then (
core s)
= s1 & (
core s)
= s2 by
A2,
Th26;
hence thesis;
end;
A4:
now
let s1 be
stack of X, e be
Element of X such that
A5:
P[s1];
thus
P[(
push (e,s1))]
proof
let s2;
assume
A6: (
push (e,s1))
in (
coset s) & s2
in (
coset s) &
|.(
push (e,s1)).|
=
|.s2.|;
then
A7:
|.s2.|
= (
<*e*>
^
|.s1.|) by
Th8;
then not
emp s2 by
Th5;
then
A8: s2
= (
push ((
top s2),(
pop s2))) by
Def9;
then
A9: s1
in (
coset s) & (
pop s2)
in (
coset s) by
A6,
Th20;
|.s2.|
= (
<*(
top s2)*>
^
|.(
pop s2).|) by
A8,
Th8;
then e
= (
|.s2.|
. 1) & (
|.s2.|
. 1)
= (
top s2) &
|.s1.|
=
|.(
pop s2).| by
A7,
FINSEQ_1: 41,
HILBERT2: 2;
hence thesis by
A5,
A8,
A9;
end;
end;
P[s1] from
INDsch(
A1,
A4);
hence thesis;
end;
theorem ::
STACKS_1:33
Th33: ex s st ((
coset s1)
/\ (
Class ((
==_ X),s2)))
=
{s}
proof
consider s such that
A1:
|.s.|
=
|.s2.| & s
in (
coset s1) by
Th30;
take s;
thus ((
coset s1)
/\ (
Class ((
==_ X),s2)))
c=
{s}
proof
let x be
object;
assume
A2: x
in ((
coset s1)
/\ (
Class ((
==_ X),s2)));
then
A3: x
in (
coset s1) & x
in (
Class ((
==_ X),s2)) by
XBOOLE_0:def 4;
reconsider x as
stack of X by
A2;
[s2, x]
in (
==_ X) by
A3,
EQREL_1: 18;
then s2
== x by
Def16;
then
|.s2.|
=
|.x.|;
then s
= x by
A1,
A3,
Th32;
hence thesis by
TARSKI:def 1;
end;
s
== s2 by
A1;
then
[s2, s]
in (
==_ X) by
Def16;
then s
in (
Class ((
==_ X),s2)) by
EQREL_1: 18;
then
{s}
c= (
Class ((
==_ X),s2)) &
{s}
c= (
coset s1) by
A1,
ZFMISC_1: 31;
hence thesis by
XBOOLE_1: 19;
end;
begin
definition
let X;
::
STACKS_1:def20
func X
/== ->
strict
StackSystem means
:
Def20: 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 be
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
proof
let X1,X2 be
strict
StackSystem such that
A1: the
carrier of X1
= the
carrier of X & the
carrier' of X1
= (
Class (
==_ X)) & the
s_empty of X1
=
{the
s_empty of X} & the
s_push of X1
= (the
s_push of X
/\/ (
==_ X)) & the
s_pop of X1
= ((the
s_pop of X
+* (
id the
s_empty of X))
/\/ (
==_ X)) and
A2: for f be
Choice_Function of (
Class (
==_ X)) holds the
s_top of X1
= ((the
s_top of X
* f)
+* (the
s_empty of X, the
Element of the
carrier of X)) and
A3: the
carrier of X2
= the
carrier of X & the
carrier' of X2
= (
Class (
==_ X)) & the
s_empty of X2
=
{the
s_empty of X} & the
s_push of X2
= (the
s_push of X
/\/ (
==_ X)) & the
s_pop of X2
= ((the
s_pop of X
+* (
id the
s_empty of X))
/\/ (
==_ X)) and
A4: for f be
Choice_Function of (
Class (
==_ X)) holds the
s_top of X2
= ((the
s_top of X
* f)
+* (the
s_empty of X, the
Element of the
carrier of X));
set f = the
Choice_Function of (
Class (
==_ X));
the
s_top of X1
= ((the
s_top of X
* f)
+* (the
s_empty of X, the
Element of the
carrier of X)) & the
s_top of X2
= ((the
s_top of X
* f)
+* (the
s_empty of X, the
Element of the
carrier of X)) by
A2,
A4;
hence thesis by
A1,
A3;
end;
existence
proof
set f = the
Choice_Function of (
Class (
==_ X));
not
{}
in (
Class (
==_ X));
then
A5: f is
Function of (
Class (
==_ X)), (
union (
Class (
==_ X))) by
ORDERS_1: 90;
A6: (
union (
Class (
==_ X)))
= the
carrier' of X by
EQREL_1:def 4;
then
reconsider f as
Function of (
Class (
==_ X)), the
carrier' of X by
A5;
consider s such that
A7:
emp s by
Th2;
A8: (
Class ((
==_ X),s))
= the
s_empty of X by
A7,
Th19;
reconsider E = (
Class ((
==_ X),s)) as
Element of (
Class (
==_ X)) by
EQREL_1:def 3;
set g = (the
s_top of X
* f);
take X1 =
StackSystem (# the
carrier of X, (
Class (
==_ X)),
{E}, (the
s_push of X
/\/ (
==_ X)), ((the
s_pop of X
+* (
id the
s_empty of X))
/\/ (
==_ X)), (g
+* (the
s_empty of X, the
Element of the
carrier of X)) #);
thus the
carrier of X1
= the
carrier of X & the
carrier' of X1
= (
Class (
==_ X)) & the
s_empty of X1
=
{the
s_empty of X} & the
s_push of X1
= (the
s_push of X
/\/ (
==_ X)) & the
s_pop of X1
= ((the
s_pop of X
+* (
id the
s_empty of X))
/\/ (
==_ X)) by
A7,
Th19;
let h be
Choice_Function of (
Class (
==_ X));
not
{}
in (
Class (
==_ X));
then h is
Function of (
Class (
==_ X)), (
union (
Class (
==_ X))) by
ORDERS_1: 90;
then
reconsider h0 = h as
Function of (
Class (
==_ X)), the
carrier' of X by
A6;
now
let a be
Element of (
Class (
==_ X));
consider s1 such that
A9: a
= (
Class ((
==_ X),s1)) by
EQREL_1: 36;
per cases ;
suppose
emp s1;
then s1
in the
s_empty of X & (
dom g)
= (
Class (
==_ X)) & (
dom (the
s_top of X
* h0))
= (
Class (
==_ X)) by
FUNCT_2:def 1;
then
A10: a
= E & E
in (
dom g) & E
in (
dom (the
s_top of X
* h0)) by
A8,
A9,
EQREL_1: 23;
then ((g
+* (the
s_empty of X, the
Element of the
carrier of X))
. a)
= the
Element of the
carrier of X by
A8,
FUNCT_7: 31;
hence ((g
+* (the
s_empty of X, the
Element of the
carrier of X))
. a)
= (((the
s_top of X
* h0)
+* (the
s_empty of X, the
Element of the
carrier of X))
. a) by
A8,
A10,
FUNCT_7: 31;
end;
suppose
A11: not
emp s1;
then s1
nin E by
A8;
then
A12: a
<> E by
A9,
EQREL_1: 23;
{}
nin (
Class (
==_ X));
then (f
. a)
in a & (h
. a)
in a by
ORDERS_1: 89;
then
[s1, (f
. a)]
in (
==_ X) &
[s1, (h
. a)]
in (
==_ X) by
A9,
EQREL_1: 18;
then s1
== (f
. a) & s1
== (h0
. a) by
Def16;
then (f
. a)
== (h0
. a) & not
emp (f
. a) by
A11,
Th14;
then (
top (f
. a))
= (
top (h0
. a)) by
Th18;
then (g
. a)
= (
top (h0
. a)) by
FUNCT_2: 15;
then (g
. a)
= ((the
s_top of X
* h0)
. a) by
FUNCT_2: 15;
then ((g
+* (the
s_empty of X, the
Element of the
carrier of X))
. a)
= ((the
s_top of X
* h0)
. a) by
A8,
A12,
FUNCT_7: 32;
hence ((g
+* (the
s_empty of X, the
Element of the
carrier of X))
. a)
= (((the
s_top of X
* h0)
+* (the
s_empty of X, the
Element of the
carrier of X))
. a) by
A8,
A12,
FUNCT_7: 32;
end;
end;
hence the
s_top of X1
= ((the
s_top of X
* h)
+* (the
s_empty of X, the
Element of the
carrier of X)) by
FUNCT_2: 63;
end;
end
registration
let X;
cluster (X
/== ) -> non
empty non
void;
coherence
proof
the
carrier of (X
/== )
= the
carrier of X & the
carrier' of (X
/== )
= (
Class (
==_ X)) by
Def20;
hence thesis;
end;
end
theorem ::
STACKS_1:34
Th34: for S be
stack of (X
/== ) holds ex s st S
= (
Class ((
==_ X),s))
proof
let S be
stack of (X
/== );
the
carrier' of (X
/== )
= (
Class (
==_ X)) by
Def20;
then S
in (
Class (
==_ X));
then ex x be
object st x
in the
carrier' of X & S
= (
Class ((
==_ X),x)) by
EQREL_1:def 3;
hence thesis;
end;
theorem ::
STACKS_1:35
Th35: (
Class ((
==_ X),s)) is
stack of (X
/== )
proof
the
carrier' of (X
/== )
= (
Class (
==_ X)) by
Def20;
hence thesis by
EQREL_1:def 3;
end;
theorem ::
STACKS_1:36
Th36: for S be
stack of (X
/== ) st S
= (
Class ((
==_ X),s)) holds
emp s iff
emp S
proof
let S be
stack of (X
/== );
assume
A1: S
= (
Class ((
==_ X),s));
consider s1 such that
A2:
emp s1 by
Th2;
emp S iff S
in
{the
s_empty of X} by
Def20;
then
emp S iff S
= the
s_empty of X by
TARSKI:def 1;
then
emp S iff S
= (
Class ((
==_ X),s1)) by
A2,
Th19;
then
emp S iff
[s, s1]
in (
==_ X) by
A1,
EQREL_1: 35;
then
emp S iff s
== s1 by
Def16;
hence
emp s iff
emp S by
A2,
Th14,
Th15;
end;
theorem ::
STACKS_1:37
Th37: for S be
stack of (X
/== ) holds
emp S iff S
= the
s_empty of X
proof
let S be
stack of (X
/== );
the
carrier' of (X
/== )
= (
Class (
==_ X)) by
Def20;
then S
in (
Class (
==_ X));
then
consider x be
object such that
A1: x
in the
carrier' of X & S
= (
Class ((
==_ X),x)) by
EQREL_1:def 3;
reconsider x as
stack of X by
A1;
hereby
assume
emp S;
then
emp x by
A1,
Th36;
hence S
= the
s_empty of X by
A1,
Th19;
end;
assume S
= the
s_empty of X;
then x
in the
s_empty of X by
A1,
EQREL_1: 20;
then
emp x;
hence thesis by
A1,
Th36;
end;
theorem ::
STACKS_1:38
Th38: for S be
stack of (X
/== ), E be
Element of (X
/== ) st S
= (
Class ((
==_ X),s)) & E
= e holds (
push (e,s))
in (
push (E,S)) & (
Class ((
==_ X),(
push (e,s))))
= (
push (E,S))
proof
let S be
stack of (X
/== );
let E be
Element of (X
/== );
assume
A1: S
= (
Class ((
==_ X),s));
assume
A2: E
= e;
A3: s
in S by
A1,
EQREL_1: 20;
A4: S
in (
Class (
==_ X)) by
A1,
EQREL_1:def 3;
A5: the
s_push of X is
BinOp of the
carrier of X, the
carrier' of X, (
==_ X)
proof
let x be
Element of X, y1,y2 be
stack of X;
assume
[y1, y2]
in (
==_ X);
then y1
== y2 by
Def16;
then (
push (x,y1))
== (
push (x,y2)) by
Th16;
hence
[(the
s_push of X
. (x,y1)), (the
s_push of X
. (x,y2))]
in (
==_ X) by
Def16;
end;
(
push (E,S))
= ((the
s_push of X
/\/ (
==_ X))
. (E,S)) by
Def20
.= (
Class ((
==_ X),(
push (e,s)))) by
A2,
A3,
A4,
A5,
Def2;
hence thesis by
EQREL_1: 20;
end;
theorem ::
STACKS_1:39
Th39: for S be
stack of (X
/== ) st S
= (
Class ((
==_ X),s)) & not
emp s holds (
pop s)
in (
pop S) & (
Class ((
==_ X),(
pop s)))
= (
pop S)
proof
set p = the
s_pop of X;
set i = (
id the
s_empty of X);
let S be
stack of (X
/== );
assume
A1: S
= (
Class ((
==_ X),s));
assume
A2: not
emp s;
A3: s
in S by
A1,
EQREL_1: 20;
A4: S
in (
Class (
==_ X)) by
A1,
EQREL_1:def 3;
A5: (
dom i)
= the
s_empty of X;
A6: (p
+* i) is
UnOp of the
carrier' of X, (
==_ X)
proof
let y1,y2 be
stack of X;
assume
A7:
[y1, y2]
in (
==_ X);
then
A8: y1
== y2 by
Def16;
per cases ;
suppose
A9: not
emp y1;
then not
emp y2 by
A8,
Th14;
then y1
nin the
s_empty of X & y2
nin the
s_empty of X by
A9;
then
A10: ((p
+* i)
. y1)
= (p
. y1) & ((p
+* i)
. y2)
= (p
. y2) by
A5,
FUNCT_4: 11;
(
pop y1)
== (
pop y2) by
A8,
A9,
Th17;
hence
[((p
+* i)
. y1), ((p
+* i)
. y2)]
in (
==_ X) by
A10,
Def16;
end;
suppose
A11:
emp y1;
then
emp y2 by
A8,
Th14;
then y1
in the
s_empty of X & y2
in the
s_empty of X by
A11;
then ((p
+* i)
. y1)
= (i
. y1) & (i
. y1)
= y1 & ((p
+* i)
. y2)
= (i
. y2) & (i
. y2)
= y2 by
A5,
FUNCT_1: 18,
FUNCT_4: 13;
hence thesis by
A7;
end;
end;
A12: s
nin the
s_empty of X by
A2;
(
pop S)
= (((p
+* i)
/\/ (
==_ X))
. S) by
Def20
.= (
Class ((
==_ X),((p
+* i)
. s))) by
A3,
A4,
A6,
FILTER_1:def 3
.= (
Class ((
==_ X),(
pop s))) by
A5,
A12,
FUNCT_4: 11;
hence thesis by
EQREL_1: 20;
end;
theorem ::
STACKS_1:40
Th40: for S be
stack of (X
/== ) st S
= (
Class ((
==_ X),s)) & not
emp s holds (
top S)
= (
top s)
proof
set t = the
s_top of X;
set A = the
s_empty of X;
set e = the
Element of the
carrier of X;
let S be
stack of (X
/== );
assume
A1: S
= (
Class ((
==_ X),s));
assume
A2: not
emp s;
then not
emp S by
A1,
Th36;
then
A3: S
<> A by
Th37;
set f = the
Choice_Function of (
Class (
==_ X));
A4: S
in (
Class (
==_ X)) &
{}
nin (
Class (
==_ X)) by
A1,
EQREL_1:def 3;
then
A5: (f
. S)
in S by
ORDERS_1: 89;
then
reconsider x = (f
. S) as
stack of X by
A1;
[s, x]
in (
==_ X) by
A1,
A5,
EQREL_1: 18;
then
A6: s
== x by
Def16;
A7: (
dom f)
= (
Class (
==_ X)) by
A4,
RLVECT_3: 28;
the
s_top of (X
/== )
= ((t
* f)
+* (A,e)) by
Def20;
hence (
top S)
= ((t
* f)
. S) by
A3,
FUNCT_7: 32
.= (
top x) by
A4,
A7,
FUNCT_1: 13
.= (
top s) by
A6,
A2,
Th18;
end;
registration
let X;
cluster (X
/== ) ->
pop-finite;
coherence
proof
let f be
sequence of the
carrier' of (X
/== );
set s1 = the
stack of X;
defpred
P[
object,
object] means ex B be
set st B
= $1 & $2
in ((
coset s1)
/\ B);
A1: for x be
object st x
in (
Class (
==_ X)) holds ex y be
object st y
in the
carrier' of X &
P[x, y]
proof
let x be
object;
assume x
in (
Class (
==_ X));
then
consider s2 such that
A2: x
= (
Class ((
==_ X),s2)) by
EQREL_1: 36;
consider s such that
A3: ((
coset s1)
/\ (
Class ((
==_ X),s2)))
=
{s} by
Th33;
take s;
thus s
in the
carrier' of X;
reconsider B = x as
set by
TARSKI: 1;
take B;
thus B
= x;
thus s
in ((
coset s1)
/\ B) by
A2,
A3,
TARSKI:def 1;
end;
consider g be
Function such that
A4: (
dom g)
= (
Class (
==_ X)) & (
rng g)
c= the
carrier' of X & for x be
object st x
in (
Class (
==_ X)) holds
P[x, (g
. x)] from
FUNCT_1:sch 6(
A1);
A5: the
carrier' of (X
/== )
= (
Class (
==_ X)) by
Def20;
then
reconsider g as
Function of the
carrier' of (X
/== ), the
carrier' of X by
A4,
FUNCT_2: 2;
consider i, s such that
A6: ((g
* f)
. i)
= s & ( not
emp s implies ((g
* f)
. (i
+ 1))
<> (
pop s)) by
Def8;
reconsider S = (
Class ((
==_ X),s)) as
stack of (X
/== ) by
A5,
EQREL_1:def 3;
take i, S;
consider s2 such that
A7: (f
. i)
= (
Class ((
==_ X),s2)) by
A5,
EQREL_1: 36;
i
in
NAT by
ORDINAL1:def 12;
then
A8: s
= (g
. (f
. i)) by
A6,
FUNCT_2: 15;
P[(f
. i), (g
. (f
. i))] by
A4,
A5;
then s
in ((
coset s1)
/\ (f
. i)) by
A8;
then
A9: s
in (
coset s1) & s
in (f
. i) by
XBOOLE_0:def 4;
hence (f
. i)
= S by
A7,
EQREL_1: 23;
assume
A10: not
emp S;
then
A11: not
emp s by
Th36;
assume
A12: (f
. (i
+ 1))
= (
pop S);
then
A13: (f
. (i
+ 1))
= (
Class ((
==_ X),(
pop s))) by
A11,
Th39;
set s3 = (g
. (f
. (i
+ 1)));
consider s4 be
stack of X such that
A14: ((
coset s1)
/\ (f
. (i
+ 1)))
=
{s4} by
A13,
Th33;
(
pop s)
in (
coset s1) & (
pop s)
in (
pop S) & (
pop S)
= (f
. (i
+ 1)) by
A9,
A12,
A11,
Def17,
Th39;
then
A15: (
pop s)
in
{s4} by
A14,
XBOOLE_0:def 4;
P[(f
. (i
+ 1)), (g
. (f
. (i
+ 1)))] by
A4,
A5;
then s3
in ((
coset s1)
/\ (f
. (i
+ 1)));
then s3
= s4 & (
pop s)
= s4 by
A14,
A15,
TARSKI:def 1;
hence thesis by
A6,
A10,
Th36,
FUNCT_2: 15;
end;
cluster (X
/== ) ->
push-pop;
coherence
proof
let S be
stack of (X
/== );
consider s such that
A16: S
= (
Class ((
==_ X),s)) by
Th34;
assume not
emp S;
then
A17: not
emp s by
A16,
Th36;
reconsider P = (
Class ((
==_ X),(
pop s))) as
stack of (X
/== ) by
Th35;
reconsider E = (
top s) as
Element of (X
/== ) by
Def20;
thus S
= (
Class ((
==_ X),(
push ((
top s),(
pop s))))) by
A16,
A17,
Def9
.= (
push (E,P)) by
Th38
.= (
push ((
top S),P)) by
A16,
A17,
Th40
.= (
push ((
top S),(
pop S))) by
A16,
A17,
Th39;
end;
cluster (X
/== ) ->
top-push;
coherence
proof
let S be
stack of (X
/== ), E be
Element of (X
/== );
consider s such that
A18: S
= (
Class ((
==_ X),s)) by
Th34;
reconsider e = E as
Element of X by
Def20;
reconsider P = (
Class ((
==_ X),(
push (e,s)))) as
stack of (X
/== ) by
Th35;
A19: not
emp (
push (e,s)) by
Def12;
thus E
= (
top (
push (e,s))) by
Def10
.= (
top P) by
A19,
Th40
.= (
top (
push (E,S))) by
A18,
Th38;
end;
cluster (X
/== ) ->
pop-push;
coherence
proof
let S be
stack of (X
/== ), E be
Element of (X
/== );
consider s such that
A20: S
= (
Class ((
==_ X),s)) by
Th34;
reconsider e = E as
Element of X by
Def20;
reconsider P = (
Class ((
==_ X),(
push (e,s)))) as
stack of (X
/== ) by
Th35;
A21: not
emp (
push (e,s)) by
Def12;
thus S
= (
Class ((
==_ X),(
pop (
push (e,s))))) by
A20,
Def11
.= (
pop P) by
A21,
Th39
.= (
pop (
push (E,S))) by
A20,
Th38;
end;
cluster (X
/== ) ->
push-non-empty;
coherence
proof
let S be
stack of (X
/== ), E be
Element of (X
/== );
consider s such that
A22: S
= (
Class ((
==_ X),s)) by
Th34;
reconsider e = E as
Element of X by
Def20;
reconsider P = (
Class ((
==_ X),(
push (e,s)))) as
stack of (X
/== ) by
Th35;
not
emp (
push (e,s)) by
Def12;
then not
emp P by
Th36;
hence thesis by
A22,
Th38;
end;
end
theorem ::
STACKS_1:41
Th41: for S be
stack of (X
/== ) st S
= (
Class ((
==_ X),s)) holds
|.S.|
=
|.s.|
proof
defpred
P[
stack of X] means for S be
stack of (X
/== ) st S
= (
Class ((
==_ X),$1)) holds
|.S.|
=
|.$1.|;
A1:
emp s1 implies
P[s1]
proof
assume
A2:
emp s1;
let S be
stack of (X
/== );
assume S
= (
Class ((
==_ X),s1));
then
emp S by
A2,
Th36;
then
|.S.|
=
{} by
Th5;
hence thesis by
A2,
Th5;
end;
A3:
P[s1] implies
P[(
push (e,s1))]
proof
assume
A4:
P[s1];
reconsider E = e as
Element of (X
/== ) by
Def20;
let S be
stack of (X
/== );
assume
A5: S
= (
Class ((
==_ X),(
push (e,s1))));
reconsider P = (
Class ((
==_ X),s1)) as
stack of (X
/== ) by
Th35;
S
= (
push (E,P)) by
A5,
Th38;
hence
|.S.|
= (
<*E*>
^
|.P.|) by
Th8
.= (
<*e*>
^
|.s1.|) by
A4
.=
|.(
push (e,s1)).| by
Th8;
end;
thus
P[s] from
INDsch(
A1,
A3);
end;
registration
let X;
cluster (X
/== ) ->
proper-for-identity;
coherence
proof
let S1,S2 be
stack of (X
/== );
consider s1 such that
A1: S1
= (
Class ((
==_ X),s1)) by
Th34;
consider s2 such that
A2: S2
= (
Class ((
==_ X),s2)) by
Th34;
assume
|.S1.|
=
|.S2.|;
then
|.s1.|
=
|.S2.| by
A1,
Th41
.=
|.s2.| by
A2,
Th41;
then s1
== s2;
then
[s1, s2]
in (
==_ X) by
Def16;
then s2
in S1 by
A1,
EQREL_1: 18;
hence thesis by
A1,
A2,
EQREL_1: 23;
end;
end
registration
cluster
proper-for-identity for
StackAlgebra;
existence
proof
take ( the
StackAlgebra
/== );
thus thesis;
end;
end
begin
definition
let X1,X2 be
StackAlgebra;
let F,G be
Function;
::
STACKS_1:def21
pred F,G
form_isomorphism_between X1,X2 means (
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 be
stack of X1, s2 be
stack of X2 st s2
= (G
. s1) holds (
emp s1 iff
emp s2) & ( not
emp s1 implies (
pop s2)
= (G
. (
pop s1)) & (
top s2)
= (F
. (
top s1))) & for e1 be
Element of X1, e2 be
Element of X2 st e2
= (F
. e1) holds (
push (e2,s2))
= (G
. (
push (e1,s1)));
end
reserve X1,X2,X3 for
StackAlgebra;
reserve F,F1,F2,G,G1,G2 for
Function;
theorem ::
STACKS_1:42
((
id the
carrier of X),(
id the
carrier' of X))
form_isomorphism_between (X,X);
theorem ::
STACKS_1:43
Th43: (F,G)
form_isomorphism_between (X1,X2) implies ((F
" ),(G
" ))
form_isomorphism_between (X2,X1)
proof
assume that
A1: (
dom F)
= the
carrier of X1 & (
rng F)
= the
carrier of X2 & F is
one-to-one and
A2: (
dom G)
= the
carrier' of X1 & (
rng G)
= the
carrier' of X2 & G is
one-to-one and
A3: for s1 be
stack of X1, s2 be
stack of X2 st s2
= (G
. s1) holds (
emp s1 iff
emp s2) & ( not
emp s1 implies (
pop s2)
= (G
. (
pop s1)) & (
top s2)
= (F
. (
top s1))) & for e1 be
Element of X1, e2 be
Element of X2 st e2
= (F
. e1) holds (
push (e2,s2))
= (G
. (
push (e1,s1)));
thus (
dom (F
" ))
= the
carrier of X2 & (
rng (F
" ))
= the
carrier of X1 & (F
" ) is
one-to-one by
A1,
FUNCT_1: 33;
thus (
dom (G
" ))
= the
carrier' of X2 & (
rng (G
" ))
= the
carrier' of X1 & (G
" ) is
one-to-one by
A2,
FUNCT_1: 33;
let s1 be
stack of X2, s2 be
stack of X1;
assume s2
= ((G
" )
. s1);
then
A4: (G
. s2)
= s1 by
A2,
FUNCT_1: 35;
hence
A5:
emp s1 iff
emp s2 by
A3;
hereby
assume not
emp s1;
then (
pop s1)
= (G
. (
pop s2)) & (
top s1)
= (F
. (
top s2)) by
A3,
A5,
A4;
hence (
pop s2)
= ((G
" )
. (
pop s1)) & (
top s2)
= ((F
" )
. (
top s1)) by
A1,
A2,
FUNCT_1: 34;
end;
let e1 be
Element of X2, e2 be
Element of X1;
assume e2
= ((F
" )
. e1);
then (F
. e2)
= e1 by
A1,
FUNCT_1: 35;
then (G
. (
push (e2,s2)))
= (
push (e1,s1)) by
A3,
A4;
hence thesis by
A2,
FUNCT_1: 34;
end;
theorem ::
STACKS_1:44
Th44: (F1,G1)
form_isomorphism_between (X1,X2) & (F2,G2)
form_isomorphism_between (X2,X3) implies ((F2
* F1),(G2
* G1))
form_isomorphism_between (X1,X3)
proof
assume that
A1: (
dom F1)
= the
carrier of X1 & (
rng F1)
= the
carrier of X2 & F1 is
one-to-one and
A2: (
dom G1)
= the
carrier' of X1 & (
rng G1)
= the
carrier' of X2 & G1 is
one-to-one and
A3: for s1 be
stack of X1, s2 be
stack of X2 st s2
= (G1
. s1) holds (
emp s1 iff
emp s2) & ( not
emp s1 implies (
pop s2)
= (G1
. (
pop s1)) & (
top s2)
= (F1
. (
top s1))) & for e1 be
Element of X1, e2 be
Element of X2 st e2
= (F1
. e1) holds (
push (e2,s2))
= (G1
. (
push (e1,s1))) and
A4: (
dom F2)
= the
carrier of X2 & (
rng F2)
= the
carrier of X3 & F2 is
one-to-one and
A5: (
dom G2)
= the
carrier' of X2 & (
rng G2)
= the
carrier' of X3 & G2 is
one-to-one and
A6: for s1 be
stack of X2, s2 be
stack of X3 st s2
= (G2
. s1) holds (
emp s1 iff
emp s2) & ( not
emp s1 implies (
pop s2)
= (G2
. (
pop s1)) & (
top s2)
= (F2
. (
top s1))) & for e1 be
Element of X2, e2 be
Element of X3 st e2
= (F2
. e1) holds (
push (e2,s2))
= (G2
. (
push (e1,s1)));
thus (
dom (F2
* F1))
= the
carrier of X1 & (
rng (F2
* F1))
= the
carrier of X3 & (F2
* F1) is
one-to-one by
A1,
A4,
RELAT_1: 27,
RELAT_1: 28;
thus (
dom (G2
* G1))
= the
carrier' of X1 & (
rng (G2
* G1))
= the
carrier' of X3 & (G2
* G1) is
one-to-one by
A2,
A5,
RELAT_1: 27,
RELAT_1: 28;
let s1 be
stack of X1, s2 be
stack of X3;
reconsider s3 = (G1
. s1) as
stack of X2 by
A2,
FUNCT_1:def 3;
assume s2
= ((G2
* G1)
. s1);
then
A7: s2
= (G2
. s3) by
A2,
FUNCT_1: 13;
emp s1 iff
emp s3 by
A3;
hence
emp s1 iff
emp s2 by
A6,
A7;
hereby
assume not
emp s1;
then (
pop s3)
= (G1
. (
pop s1)) & (
top s3)
= (F1
. (
top s1)) & not
emp s3 by
A3;
then (
pop s2)
= (G2
. (G1
. (
pop s1))) & (
top s2)
= (F2
. (F1
. (
top s1))) by
A6,
A7;
hence (
pop s2)
= ((G2
* G1)
. (
pop s1)) & (
top s2)
= ((F2
* F1)
. (
top s1)) by
A1,
A2,
FUNCT_1: 13;
end;
let e1 be
Element of X1, e2 be
Element of X3;
reconsider e3 = (F1
. e1) as
Element of X2 by
A1,
FUNCT_1:def 3;
assume e2
= ((F2
* F1)
. e1);
then
A8: e2
= (F2
. e3) by
A1,
FUNCT_1: 13;
(
push (e3,s3))
= (G1
. (
push (e1,s1))) by
A3;
then (
push (e2,s2))
= (G2
. (G1
. (
push (e1,s1)))) by
A7,
A8,
A6;
hence (
push (e2,s2))
= ((G2
* G1)
. (
push (e1,s1))) by
A2,
FUNCT_1: 13;
end;
theorem ::
STACKS_1:45
Th45: (F,G)
form_isomorphism_between (X1,X2) implies for s1 be
stack of X1, s2 be
stack of X2 st s2
= (G
. s1) holds
|.s2.|
= (F
*
|.s1.|)
proof
assume that
A1: (
dom F)
= the
carrier of X1 & (
rng F)
= the
carrier of X2 & F is
one-to-one and
A2: (
dom G)
= the
carrier' of X1 & (
rng G)
= the
carrier' of X2 & G is
one-to-one and
A3: for s1 be
stack of X1, s2 be
stack of X2 st s2
= (G
. s1) holds (
emp s1 iff
emp s2) & ( not
emp s1 implies (
pop s2)
= (G
. (
pop s1)) & (
top s2)
= (F
. (
top s1))) & for e1 be
Element of X1, e2 be
Element of X2 st e2
= (F
. e1) holds (
push (e2,s2))
= (G
. (
push (e1,s1)));
reconsider F1 = F as
Function of the
carrier of X1, the
carrier of X2 by
A1,
FUNCT_2: 2;
reconsider G1 = G as
Function of the
carrier' of X1, the
carrier' of X2 by
A2,
FUNCT_2: 2;
let s1 be
stack of X1;
defpred
P[
stack of X1] means for s2 be
stack of X2 st s2
= (G
. $1) holds
|.s2.|
= (F
*
|.$1.|);
A4: for s1 be
stack of X1 st
emp s1 holds
P[s1]
proof
let s1 be
stack of X1;
assume
A5:
emp s1;
let s2 be
stack of X2;
assume s2
= (G
. s1);
then
emp s2 by
A3,
A5;
then
|.s2.|
=
{} &
|.s1.|
=
{} by
A5,
Th5;
hence
|.s2.|
= (F
*
|.s1.|);
end;
A6: for s1 be
stack of X1, e be
Element of X1 st
P[s1] holds
P[(
push (e,s1))]
proof
let s1 be
stack of X1;
let e be
Element of X1;
assume
A7:
P[s1];
let s2 be
stack of X2;
A8:
|.(G1
. s1).|
= (F
*
|.s1.|) by
A7;
A9:
<*(F1
. e)*>
= (F
*
<*e*>) by
A1,
FINSEQ_2: 34;
assume s2
= (G
. (
push (e,s1)));
then s2
= (
push ((F1
. e),(G1
. s1))) by
A3;
hence
|.s2.|
= (
<*(F1
. e)*>
^
|.(G1
. s1).|) by
Th8
.= (F
* (
<*e*>
^
|.s1.|)) by
A8,
A9,
FINSEQOP: 9
.= (F
*
|.(
push (e,s1)).|) by
Th8;
end;
thus
P[s1] from
INDsch(
A4,
A6);
end;
definition
let X1,X2 be
StackAlgebra;
::
STACKS_1:def22
pred X1,X2
are_isomorphic means ex F,G be
Function st (F,G)
form_isomorphism_between (X1,X2);
reflexivity
proof
let X;
take F = (
id the
carrier of X), G = (
id the
carrier' of X);
thus thesis;
end;
symmetry
proof
let X1, X2;
given F, G such that
A1: (F,G)
form_isomorphism_between (X1,X2);
take (F
" ), (G
" );
thus thesis by
A1,
Th43;
end;
end
theorem ::
STACKS_1:46
(X1,X2)
are_isomorphic & (X2,X3)
are_isomorphic implies (X1,X3)
are_isomorphic
proof
given F1, G1 such that
A1: (F1,G1)
form_isomorphism_between (X1,X2);
given F2, G2 such that
A2: (F2,G2)
form_isomorphism_between (X2,X3);
take (F2
* F1), (G2
* G1);
thus thesis by
A1,
A2,
Th44;
end;
theorem ::
STACKS_1:47
(X1,X2)
are_isomorphic & X1 is
proper-for-identity implies X2 is
proper-for-identity
proof
given F, G such that
A1: (F,G)
form_isomorphism_between (X1,X2);
assume
A2: X1 is
proper-for-identity;
let s1,s2 be
stack of X2;
A3: (
dom G)
= the
carrier' of X1 & (
rng G)
= the
carrier' of X2 by
A1;
then
consider q1 be
object such that
A4: q1
in (
dom G) & s1
= (G
. q1) by
FUNCT_1:def 3;
consider q2 be
object such that
A5: q2
in (
dom G) & s2
= (G
. q2) by
A3,
FUNCT_1:def 3;
reconsider q1, q2 as
stack of X1 by
A1,
A4,
A5;
A6: (
dom F)
= the
carrier of X1 & (
rng F)
= the
carrier of X2 & F is
one-to-one by
A1;
A7: (
rng
|.q1.|)
c= the
carrier of X1 & (
rng
|.q2.|)
c= the
carrier of X1;
assume
|.s1.|
=
|.s2.|;
then
A8: (F
*
|.q1.|)
=
|.s2.| by
A1,
A4,
Th45
.= (F
*
|.q2.|) by
A1,
A5,
Th45;
(
dom (F
*
|.q1.|))
= (
dom
|.q1.|) & (
dom (F
*
|.q2.|))
= (
dom
|.q2.|) by
A6,
A7,
RELAT_1: 27;
then
|.q1.|
=
|.q2.| by
A6,
A7,
A8,
FUNCT_1: 27;
then q1
== q2;
hence thesis by
A2,
A4,
A5;
end;
theorem ::
STACKS_1:48
Th48: for X be
proper-for-identity
StackAlgebra holds ex G st (for s be
stack of X holds (G
. s)
=
|.s.|) & ((
id the
carrier of X),G)
form_isomorphism_between (X,(
StandardStackSystem the
carrier of X))
proof
let X be
proper-for-identity
StackAlgebra;
deffunc
F(
stack of X) =
|.$1.|;
consider G be
Function of the
carrier' of X, (the
carrier of X
* ) such that
A1: for s be
stack of X holds (G
. s)
=
F(s) from
FUNCT_2:sch 4;
take G;
thus for s be
stack of X holds (G
. s)
=
|.s.| by
A1;
set F = (
id the
carrier of X);
set X2 = (
StandardStackSystem the
carrier of X);
set A = the
carrier of X;
A2: the
carrier of X2
= A & the
carrier' of X2
= (A
* ) & for s be
stack of X2 holds (
emp s iff s is
empty) & for g be
FinSequence st g
= s holds ( not
emp s implies (
top s)
= (g
. 1) & (
pop s)
= (
Del (g,1))) & (
emp s implies (
top s)
= the
Element of X2 & (
pop s)
=
{} ) & for e be
Element of X2 holds (
push (e,s))
= (
<*e*>
^ g) by
Def7;
thus (
dom F)
= the
carrier of X & (
rng F)
= the
carrier of X2 & F is
one-to-one by
A2;
thus
A3: (
dom G)
= the
carrier' of X by
FUNCT_2:def 1;
thus (
rng G)
= the
carrier' of X2
proof
thus (
rng G)
c= the
carrier' of X2 by
A2;
let x be
object;
assume x
in the
carrier' of X2;
then
reconsider x as
Element of (A
* ) by
Def7;
consider s be
stack of X such that
A4:
|.s.|
= x by
Th12;
x
= (G
. s) by
A1,
A4;
hence thesis by
A3,
FUNCT_1:def 3;
end;
thus G is
one-to-one
proof
let x,y be
object;
assume x
in (
dom G) & y
in (
dom G);
then
reconsider s1 = x, s2 = y as
stack of X;
assume (G
. x)
= (G
. y);
then
|.s1.|
= (G
. y) by
A1
.=
|.s2.| by
A1;
then s1
== s2;
hence x
= y by
Def15;
end;
let s1 be
stack of X, s2 be
stack of X2;
assume s2
= (G
. s1);
then
A5: s2
=
|.s1.| by
A1;
hereby
assume
emp s1;
then
|.s1.|
=
{} by
Th5;
hence
emp s2 by
A5,
Def7;
end;
now
assume
emp s2;
then s2
=
{} by
Def7;
hence
emp s1 by
A5,
Th10;
end;
hereby
assume
A7: not
emp s1;
thus (
pop s2)
= (
Del (s2,1)) by
A7,
A6,
Def7
.=
|.(
pop s1).| by
A5,
A7,
Th7
.= (G
. (
pop s1)) by
A1;
thus (
top s2)
= (s2
. 1) by
A7,
A6,
Def7
.= (
top s1) by
A5,
A7,
Th9
.= (F
. (
top s1));
end;
let e1 be
Element of X, e2 be
Element of X2;
assume e2
= (F
. e1);
hence (
push (e2,s2))
= (
<*(F
. e1)*>
^ s2) by
Def7
.= (
<*e1*>
^ s2)
.=
|.(
push (e1,s1)).| by
A5,
Th8
.= (G
. (
push (e1,s1))) by
A1;
end;
theorem ::
STACKS_1:49
for X be
proper-for-identity
StackAlgebra holds (X,(
StandardStackSystem the
carrier of X))
are_isomorphic
proof
let X be
proper-for-identity
StackAlgebra;
consider G such that (for s be
stack of X holds (G
. s)
=
|.s.|) and
A1: ((
id the
carrier of X),G)
form_isomorphism_between (X,(
StandardStackSystem the
carrier of X)) by
Th48;
take (
id the
carrier of X), G;
thus thesis by
A1;
end;